5th Kurt Gödel Colloquium, KGC '97 Vienna, Austria, August 25–29, 1997 Proceedings
Techniques for equational reasoning are a key component in many automated theorem provers and interactive proof and verification systems. A notable recent success in equational theorem proving has been the solution of an open problem (the “Robbins conjecture”) by William McCune with his prover Eqp [13]. Eqp is one of many equational theorem provers that use completion as the main deductive...
The tree isomorphism problem is the problem of determining whether two trees are isomorphic. The tree canonization problem is the problem of producing a canonical tree isomorphic to a given tree. The tree comparison problem is the problem of determining whether one tree is less than a second tree in a natural ordering on trees. We present alternating logarithmic time algorithms for the tree isomorphism...
We examine a new logical system, capturing the intuition of ‘most’ by means of generalised quantifiers over ultrafilters, with the aim of providing a basis for generic reasoning. This monotonic ultrafilter logic is a conservative extension of classical first-order logic, with which it shares several properties, including a simple sound and complete deductive system. For reasoning about generic objects,...
These two introspective cognitive experiments have shown how the rational imagination can be a satisfactory mental arena for the conduct of rigorous mathematical thinking. The diagrams and other representative imagery used in such thinking need not be external and public, but are capable of being privately constructed, viewed, and analyzed “in the mind's eye”. The conclusion I draw from this and other...
We discuss the general scheme of building resolution calculi (also called the inverse method) originating from S. Maslov and G. Mints. A survey of resolution calculi for various nonclassical logic is presented, along with several common properties these calculi possess.
This talk, in the first part, will overview the main advances in the area of subtyping for the simply typed lambda calculus. In the second part of the talk we will propose a new system of notations for types, which we call alternating direct acyclic graphs, and show that for a system of sybtype inequalities over a lattice, if it has a solution then there is a solution whose alternating dag is of polynomial...
We present a new proof-theoretic approach to bounding the complexity of the decision problem for propositional modal logics. We formalize logics in a uniform way as sequent systems and then restrict the structural rules for particular systems. This, combined with an analysis of the accessibility relation of the corresponding Kripke structures, yields decision procedures with bounded space requirements...
We give a precise characterization of parameter free Σ n and II n induction schemata, IΣ − n and I II − n , in terms of reflection principles. This allows us to show that I II − n+1 is conservative over IΣ − n w.r.t. boolean combinations of Σ n+1 sentences,...
Rice's Theorem says that every nontrivial semantic property of programs is undecidable. It this spirit we show the following: Every nontrivial absolute (gap, relative) counting property of circuits is UP-hard with respect to polynomial-time Turing reductions.
In this work we establish some syntactical and semantical links between Łukasiewicz Logics and Linear Logic. First we introduce a new sequent calculus of infinite-valued Łukasiewicz Logic by adding a new rule of inference to those of Affine Linear Logic. The only axioms of this calculus have the form A ⊢ A. Then we compare the (provability) semantics of both logics, respectively given by MV-algebras...
As modern Automated Deduction systems rely heavily on the use of a machine-oriented representation of a given problem, together with sophisticated redundancy-avoiding techniques, a major task in convincing human users of the correctness of automatically generated proofs is the intelligible representation of these proofs. In this paper, we propose the use of the cut-rule in the human-oriented presentation...
NaDSyL, a Natural Deduction based Symbolic Logic, and some of its applications are briefly described. The semantics of NaDSyL is based on the term models of the lambda calculus and is motivated by the belief that a confusion of use and mention is the source of the paradoxes. Proofs of the soundness, completeness and the eliminability of cut are sketched along with three applications: The foundations...
We prove that the strong Markov's rule with only set parameters is admissible in the full set theory with intuitionistic logic mis|The work was supported by Reseach Scientific Foundation of Russian Ministry of Transport
We define formally the notion of invariant defM.inability in a logic $${\cal L}$$ and study it systematically. We relate it to other notions of definability (implicit definability, Δ-definability and definability with built-in relations) and establish connections between them. In descriptive complexity theory, invariant definability is mostly used with a linear order (or a successor relation)...
Finding computationally valuable representations of models of predicate logic formulas is an important issue in the field of automated theorem proving, e.g. for automated model building or semantic resolution. In this article we treat the problem of representing single models independently of building them and discuss the power of different mechanisms for this purpose. We start with investigating...
Recently, several different sound and complete tableau calculi were introduced, all sharing the idea to use a selection function and so-called restart clauses: A-ordered tableaux, tableaux with selection function, and strict restart model elimination. We present two new sound and complete abstract tableau calculi which generalize these on the ground level. This makes differences and similarities between...
Two arithmetic constructive theories based on Dialectica interpretation are introduced and studied in the paper. For an arithmetic formula A let A D be its Dialectica interpretation in the language of arithmetic in all finite types. The translation (A D)° of A D back into the language of first-order arithmetic using the system HRO of hereditary recursive operations is...
The paper describes a class of FC-sequents of a restricted first order linear temporal logic with “next” and “always”. It is shown that the first order linear temporal logic is finitary complete for FC-sequents. If FC-sequents are logically decidable, i.e., all sequents, constructed from all possible subformulas of logical formulas of FC-sequents are decidable in first-order logic, then FC-sequents...