Third Kurt Gödel Colloquium, KGC'93 Brno, Czech Republic, August 24–27, 1993 Proceedings
We provide a logical specification of set predicates findall and bagof of Prolog. The specification is given in proof theoretic terms, and pertains to any SLD-resolution based language. The order dependent aspects, relevant for languages embodying a sequential proof search strategy (possibly with side effects), can be added in an orthogonal way. The specification also allows us to prove that bagof...
Methods originating in theoretical computer science for showing that certain decision problems are NP-complete have also been used to show that certain compactness theorems are equivalent in ZF set theory to the Boolean Prime Ideal Theorem (BPI). Conversely, there is some evidence that set theoretic methods connnected with research on BPI may prove useful in computer science. We survey what is known...
Twelve years of work on nonmonotonic logic has certainly increased our understanding of the area. However, given a problem in which nonmonotonic reasoning is called for, it is far from clear how one should go about modeling the problem using the various approaches. We explore this issue in the context on two of the best-known approaches, Reiter's default logic [Rei80] and Moore's autoepistemic logic...
The paper contains a survey of results in various areas of logic and theoretical computer science which seem to have similar logical structure. The author believes that similarity is not restricted to similar frasing of results and that many of the results described below can be proved in a uniform way.
We discuss the logics of the operators “p is a proof of A” and “p is a proof containing A” for the standard Gödel proof predicate in Peano Arithmetic. Decidability and arithmetical completeness of these logics are proved. We use the same semantics as for the Provability Logic where the operator “A is provable” is studied.
We show that superposition, a restricted form of paramodulation, can be combined with specifically designed simplification rules such that it becomes a decision procedure for the monadic class with equality. The completeness of the method follows from a general notion of redundancy for clauses and superposition inferences.
A model of computation with access to ℝ is suggested that is more restricted than, say fapC(ℝ) in [10]. In particular ℝ is treated as an accessory to the computer rather than an internal component. This has the desirable properties of a definability theorem and a parameterisation theorem for real algebraic numbers. The geometric properties of halting sets indicate the weakness of the theory. Some...
In this paper we have a closer look at one of the rules of the tableau calculus presented in [3], called the δ-rule, and the modification of this rule, that has been proved to be sound and complete in [6], called the δ +-rule, which uses fewer free variables. We show that, an even more liberalized version, the $$\delta ^{ + ^ + }$$ -rule, that in addition reduces the number of different...
In this work, we provide a presentation of classical and intuitionistic logics in a natural deduction style, making a clear distinction between extra-logical axioms and assumptions. Some important theorems about these presentations were proved — cut-elimination, consistency and completeness. Moreover, it was proved that the consequence relations defined for these logics have some interesting properties:...
The evaluation of a goal for a logic program can be viewed as the search for an answer, written in the constraints language, that correctly implies the goal. We propose a small set of inference rules, correct w.r.t. the completion of a program and the Clark equational theory, which is strong enough to compute a complete set of answers for extended programs over the Herbrand constraint system. The...
We propose techniques to provide calculi based on the connection method with a possibility to preclude infinite loops. We extend previous work — proposed in the field of Logic Programming — concerning the detection of infinite loops during the proof of Horn formulas. On the one hand, we present a technique to be integrated into connection calculi for full first-order logic. On the other hand, we show...
We prove that stability is undecidable for dynamical systems whose right-hand side is explicitly written in the language of elementary analysis.
We construct the exponential graph of a proof π in (second order) linear logic, an artefact displaying the interdependencies of exponentials in π. Within this graph superfluous exponentials are defined, the removal of which is shown to yield a correct proof π▹ with essentially the same set of reductions. Applications to intuitionistic and classical proofs are given by means of reduction-preserving...
In this paper, we introduce a resolution calculus extended by a function introduction rule and by a tautology introduction rule. As opposed to most resolution refinements where tautology deletion does not lengthen a refutation, removing tautologies may disable short refutations if extended resolution calculi are applied. Moreover, the introduction of tautologies may strengthen a resolution calculus...