Heuristic for avoiding skolemization in theorem proving.
Pevac, Irena (1985)
Publications de l'Institut Mathématique. Nouvelle Série
Similarity:
Displaying similar documents to “On global induction mechanisms in a -calculus with explicit approximations”
Heuristic for avoiding skolemization in theorem proving.
On sequent calculi for intuitionistic propositional logic
Vítězslav Švejdar (2006)
Commentationes Mathematicae Universitatis Carolinae
Similarity:
The well-known Dyckoff's 1992 calculus/procedure for intuitionistic propositional logic is considered and analyzed. It is shown that the calculus is Kripke complete and the procedure in fact works in polynomial space. Then a multi-conclusion intuitionistic calculus is introduced, obtained by adding one new rule to known calculi. A simple proof of Kripke completeness and polynomial-space decidability of this calculus is given. An upper bound on the depth of a Kripke counter-model is...
Representation of metamorphosis grammar in logic grammar: Proof trees and their lengths.
Prešić, Marica D. (1994)
Publications de l'Institut Mathématique. Nouvelle Série
Similarity:
Semantics of value recursion for monadic input/output
Levent Erkök, John Launchbury, Andrew Moran (2002)
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
Similarity:
Monads have been employed in programming languages for modeling various language features, most importantly those that involve side effects. In particular, Haskell’s IO monad provides access to I/O operations and mutable variables, without compromising referential transparency. Cyclic definitions that involve monadic computations give rise to the concept of value-recursion, where the fixed-point computation takes place only over the values, without repeating or losing effects. In this...
Experimental analysis of some computation rules in a simple parallel reasoning system for the ALC description logic
Adam Meissner (2011)
International Journal of Applied Mathematics and Computer Science
Similarity:
A computation rule determines the order of selecting premises during an inference process. In this paper we empirically analyse three particular computation rules in a tableau-based, parallel reasoning system for the ALC description logic, which is built in the relational programming model in the Oz language. The system is constructed in the lean deduction style, namely, it has the form of a small program containing only basic mechanisms, which assure soundness and completeness of reasoning....
A constructive proof of equivalence of formalism of DCG's with the formalism of type 0 phrase-structure grammars.
Prešić, Marica D., Prešić, Slaviša B. (1994)
Publications de l'Institut Mathématique. Nouvelle Série
Similarity:
A note on negative tagging for least fixed-point formulae
Dilian Gurov, Bruce Kapron (1999)
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
Similarity:
Wadge degrees of -languages of deterministic Turing machines
Victor Selivanov (2003)
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
Similarity:
We describe Wadge degrees of -languages recognizable by deterministic Turing machines. In particular, it is shown that the ordinal corresponding to these degrees is where is the first non-recursive ordinal known as the Church–Kleene ordinal. This answers a question raised in [2].
Termination checking with types
Andreas Abel (2004)
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
Similarity:
The paradigm of type-based termination is explored for functional programming with recursive data types. The article introduces , a lambda-calculus with recursion, inductive types, subtyping and bounded quantification. Decorated type variables representing approximations of inductive types are used to track the size of function arguments and return values. The system is shown to be type safe and strongly normalizing. The main novelty is a bidirectional type checking algorithm whose...