Automated Deduction — CADE-16

We reduce the provability problem of any formula of the Lambek calculus to some context-free parsing problem. This reduction, which is based on non-commutative proof-net theory, allows us to de- rive an automatic categorial deduction algorithm akin to the well-known Cocke-Kasami-Younger parsing algorithm.

We define a class of modal logics LF by uniformly extending a class of modal logics L. Each logic L is characterised by a class of first-order definable frames, but the corresponding logic LF is sometimes characterised by classes of modal frames that are not first-order definable. The class LF includes provability logics with deep arithmetical interpretations. Using Belnap’s proof-theoretical framework Display Logic we characterise the “pseudo-displayable” subclass of LF and show how to define polynomial-time transformations from each such LF into the corresponding L, and hence into first-order classical logic. Theorem provers for classical first-order logic can then be used to mechanise deduction in these “psuedo-displayable second order” modal logics.

Different variants of guarded logics (a powerful generalization of modal logics) are surveyed and the recent decidability result for guarded fixed point logic (obtained in joint work with I. Walukiewicz) is explained. The exposition given here emphasizes the tree model property of guarded logics: every satisfiable sentence has a model of bounded tree width.

We present a PSpace algorithm that decides satisfiability of the graded modal logic Gr(K_R)—a natural extension of propositional modal logic K_R by counting expressions—which plays an important role in the area of knowledge representation. The algorithm employs a tableaux approach and is the first known algorithm which meets the lower bound for the complexity of the problem. Thus, we exactly fix the complexity of the problem and refute a ExpTime-hardness conjecture. This establishes a kind of “theoretical benchmark” that all algorithmic approaches can be measured with.

Context unification is a natural variant of second order unification that represents a generalization of word unification at the same time. While second order unification is wellknown to be undecidable and word unification is decidable it is currently open if solvability of context equations is decidable. We show that solvability of systems of context equations with two context variables is decidable. The context variables may have an arbitrary number of occurrences, and the equations may contain an arbitrary number of individual variables as well. The result holds under the assumption that the first-order background signature is finite

We use the standard encoding of Boolean values in simply typed lambda calculus to develop a method of translating SAT problems for various logics into higher order matching. We obtain this way already known NP-hardness bounds for the order two and three and a new result that the fourth order matching is NEXPTIME-hard

Equational problems (i.e.: first-order formulae with quantifier prefix ∃* ∀*, whose only predicate symbol is syntactic equality) are an important tool in many areas of automated deduction, e.g.: restricting the set of ground instances of a clause via equational constraints allows the definition of stronger redundancy criteria and hence, in general, of more efficient theorem provers. Moreover, also the inference rules themselves can be restricted via constraints. In automated model building, equational problems play an important role both in the definition of an appropriate model representation and in the evaluation of clauses in such models. Also, many problems in the area of logic programming can be reduced to equational problem solving.The goal of this work is a complexity analysis of the satisfiability problem of equational problems in CNF over an infinite Herbrand universe. The main result will be a proof of the NP-completeness (and, in particular, of the NP-membership) of this problem.

We present a verifiable symbolic definite integral table lookup: a system which matches a query, comprising a definite integral with parameters and side conditions, against an entry in a verifiable table and uses a call to a library of facts about the reals in the theorem prover PVS to aid in the transformation of the table entry into an answer. Our system is able to obtain correct answers in cases where standard techniques implemented in computer algebra systems fail. We present the full model of such a system as well as a description of our prototype implementation showing the efficacy of such a system: for example, the prototype is able to obtain correct answers in cases where computer algebra systems [CAS] do not. We extend upon Fateman’s web-based table by including parametric limits of integration and queries with side conditions.

The role of decision procedures is often essential in theorem proving. Decision procedures can reduce the search space of heuristic components of a prover and increase its abilities. However, in some applications only a small number of conjectures fall within the scope of the available decision procedures. Some of these conjectures could in an informal sense fall ‘just outside’ that scope. In these situations a problem arises because lemmas have to be invoked or the decision procedure has to communicate with the heuristic component of a theorem prover. This problem is also related to the general problem of how to flexibly integrate decision procedures into heuristic theorem provers. In this paper we address such problems and describe a framework for the flexible integration of decision procedures into other proof methods. The proposed framework can be used in different theorem provers, for different theories and for different decision procedures. New decision procedures can be simply ‘plugged-in’ to the system. As an illustration, we describe an instantiation of this framework within the Clam proof-planning system, to which it is well suited. We report on some results using this implementation.

Presenting machine-generated proofs in terms adequate to the needs of a human audience is a serious challenge. One salient property of mathematical proofs as typically found in textbooks is that lines of reasoning are expressed in a rather condensed form by leaving out elementary and easily inferable, but logically necessary inference steps, while explaining involved ones in more detail. To date, automated proof presentation techniques are not able to deal with this issue in an adequate manner. Addressing this problem in a principled way, we describe an approach that successively enhances a logically self-contained proof at the assertion level through communicatively justified modifications of the original line of reasoning. These enhancements include expansion of involved theorem applications, omission of trivial justifications, compactification of intermediate inference steps, and broadening the scope of justifications to support focused argumentation, as in chains of inequations. Through incorporating these measurements, many proofs are presented in a shorter and better understandable fashion than in previous approaches.

In this paper we establish a link between satisfiability of universal sentences with respect to varieties of distributive lattices with operators and satisfiability with respect to certain classes of relational structures. We use these results for giving a method for translation to clause form of universal sentences in such varieties, and then use results from automated theorem proving to obtain decidability and complexity results for the universal theory of some such varieties.

This paper gives a new treatment of Maslov’s class K in the framework of resolution. More specifically, we show that K and the class DK consisting of disjunction of formulae in K can be decided by a resolution refinement based on liftable orderings. We also discuss relationships to other solvable and unsolvable classes.

We provide a resolution-based proof procedure for modal and description logics that improves on previous proposals in a number of important ways. First, it avoids translations into large undecidable logics, and works directly on modal or description logic formulas instead. Second, by using labeled formulas it avoids the complexities of earlier propositional resolution-based methods for modal logic. Third, it provides a method for manipulating so-called assertional information in the description logic setting. And fourth, we believe that it combines ideas from the method of prefixes used in tableaux and resolution in such a way that some of the heuristics and optimizations devised in either field are applicable.

Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It relies on the LF type theory and the judgments-as-types methodology for specification [HHP93], a constraint logic programming interpreter for implementation [Pfe91], and the meta-logic M2 for reasoning about object languages encoded in LF [SP98]. It is a significant extension and complete reimplementation of the Elf system [Pfe94].Twelf is written in Standard ML and runs under SML of New Jersey and MLWorks on Unix and Window platforms. The current version (1.2) is distributed with a complete manual, example suites, a tutorial in the form of on-line lecture notes [Pfe], and an Emacs interface. Source and binary distributions are accessible via the Twelf home page http://www.cs.cmu.edu/~twelf.

Originally developed as an automatic inductive theorem prover [2] based on res- olution and paramodulation, the inka system was redesigned in inka 4.0 in the early ’90s [8] to meet the requirements arising from its designated use in formal methods. Meanwhile several large industrial applications of the verication sup- port environment (VSE) [7] have been performed which gave rise to thousands of proof obligations to be tackled by its underlying deductive system inka.

CutRes is a system which takes as input an LK-proof with arbitrary cuts and skolemized end-sequent and gives as output an LK- proof with atomic cuts only. The elimination of cuts is performed in the following way: An unsatisfiable set of clauses C is assigned to a given LK-proof П. Any resolution refutation ψ of C then serves as a skeleton for an LK-proof Σ of the original end-sequent, containing only atomic cuts; Σ can be constructed from ψ and П by projections. Note, that a proof with atomic cuts provides the same information as a cut-free proof.

Real-world applications of theorem proving require open and modern software environments that enable modularization, distribution, inter-operability, networking, and coordination. This system description presents the MathWeb1 approach for distributed automated theorem proving that connects a wide-range of mathematical services by a common, mathematical software bus. The MathWeb system provides the functionality to turn existing theorem proving systems and tools into mathematical services that are homogeneously integrated into a networked proof development environment. The environment thus gains the services from these particular modules, but each module in turn gains from using the features of other, plugged-in components.

The verification conditions associated with concurrent systems and their invariants are usually instances of the VC-scheme, i.e., $$ \left( {\mathop \wedge \limits_{\iota = 1}^n h_i } \right) \Rightarrow c. $$

In recent years, there have been many examples of signicant formalization ef- forts in higher-order logics, including the formalization of Java [12], the veri cation of the SCI cache-coherency protocol [5], the verication of the AAMP5 avionics processor [11] in PVS [2], the verication and automated optimization of Ensemble protocols [10,7], and many others. Higher-order logics are often cho- sen for these endeavors not only because they can formalize meta-principles, but also because they retain the conciseness and intuition of the original design.

Waldmeister is an automated theorem prover for unconditional equational logic. It is based on unfailing Knuth-Bendix completion [1]. During the rst stage of development the focus was on efficient rewriting by means of indexing and space saving techniques [2, 4]. In this paper we present two aspects of our recent work which aim at improving the system with respect to performance and ease of use. Section 2 describes a more powerful hypothesis handling. In Sect. 3 we investigate the control of the proof search and outline our current component of self-adaptation to the given proof problem.

Abstraction is a useful tool in verification, often allowing the proof of correctness of a large and complex system to be reduced to showing the correctness of a much smaller simpler system. We use the Nuprl theorem prover to verify the correctness of a simple but commonly occurring abstraction. From the formal proof, we extract a program that succeeds when the abstraction method is applicable to the concrete input specification and in this case, computes the abstracted system specification. One of the main novelties of our work is our “implicit syntax” approach to formal metatheory of programming languages. Our proof relies entirely on semantic reasoning, and thus avoids the complications that often arise when formally reasoning about syntax. The semantic reasoning contains an implicit construction of the result using inductive predicates over semantic domains that express representability in a particular protocol language. This implicit construction is what allows the synthesis of a program that transforms a concrete specification to an abstract one via recursion on syntax.

In this paper, we propose a common theoretical framework for type based static analyses. The aim is the study of relationships between typing and program analysis.We present a variant of Girard’s System F called FstackП_stack≤:. We prove standard properties of FstackП_stack≤:. We show how it can be used to formalize various program analyses like binding time and dead code. We relate our work to previous analyses in terms of expressivness (often only simply typed calculi are considered) and power (more information can be inferred). FstackП: features polymorphism as well as subtyping at the level of universe extending previous author work where only universe polymorphism (on a simply typed calculus) was considered

We show that the stability requirement for a verication system yields the necessity of some sort of a reflection mechanism. However, the traditional reflection rule based on the Göodel implicit provability predicate leads to a “reflection tower” of theories which cannot be formally veried. We found natural lower and upper bounds on a metatheory capable of establishing stability of a given verication system. The paper also introduces an explicit reflection mechanism which can be veri ed internally. This circumvents the reflection tower and provides a theoretical justication for the verication process. On the practical side, the paper gives specic recommendations concerning verication of inference rules and building a veriable reflection mechanism for a theorem proving system.

Kimba is the first model generation program which implements a semi-decision procedure for nite satisability of rst-order logics with nitely many truth values. The procedure enumerates the nite models of its input and can be used to compute efficiently domain minimal models whose positive part is minimal in size. Kimba has been implemented in the constraint logic programming language Oz [6] and is based on a tableaux calculus that translates deduction problems into Constraint Satisfaction Problems (CSPs). The constraint propagators needed to solve these problems are realized as concurrent procedures that can make use of Oz’s built-in capabilities for solving CSPs.We describe the current prototype focusing on the method for generating and solving CSPs.

The logic programming language λProlog is based on the intuitionistic theory of higher-order hereditary Harrop formulas, a logic that significantly extends the theory of Horn clauses. A systematic exploitation of features in the richer logic endows λProlog with capabilities at the programming level that are not present in traditional logic programming languages. Several studies have established the value of λProlog as a language for implementing systems that manipulate formal objects such as formulas, programs, proofs and types. Towards harnessing these benefits, methods have been developed for realizing this language efficiently. This work has culminated in the description of an abstract machine and compiler based implementation scheme. An actual implementation of λProlog based on these ideas has recently been completed. The planned presentation will exhibit this system—called Teyjus—and will also illuminate the metalanguage capabilities of λProlog.

Vampire is a resolution-based theorem prover for rst-order classical logic. The current version implements ordered binary resolution with the set-of-support strategy and ordered hyperresolution. The competition version will have equality rules.Vampire owes many of its design ideas to Otter [5]. It uses a saturation-based algorithmsimilar to that described in [3], but implemented more efficiently. Some planned (but not yet implemented) extensions of Vampire are directed toward the ideas underlying the design of SPASS [9].

We describe the main characteristics of version 0.3 of the E equational theorem prover. E is based on superposition and rewriting. It features a powerful interface for specifying search guiding heuristics. We discuss some important details of the implementation and demonstrate the performance of the prover by presenting experimental results on the TPTP. Finally, we describe our future plans for improving the system.

Building a state-of-the-art theorem prover requires the combination of at least three main ingredients: good theory, clever heuristics, and the necessary engineering skills to implement it all in an efficient way. Progress in each of these ingredients interacts in different ways.On the one hand, new theoretical insights replace heuristics by more precise and effective techniques. For example, the completeness proof of basic paramod- ulation [NR95,BGLS95] shows why no inferences below Skolem functions are needed, as conjectured by McCune in [McC90]. Regarding implementation tech- niques, ad-hoc algorithms for procedures like demodulation or subsumption are replaced by efficient, re-usable, general-purpose indexing data structures for which the time and space requirements are well-known.

The Neuman-Stubblebine key exchange protocol is formalized in first-order logic and analyzed by the automated theorem prover Spass. In addition to the analysis, we develop the necessary theoretical background providing new (un)decidability results for monadic firstorder fragments involved in the analysis. The approach is applicable to a variety of security protocols and we identify possible extensions leading to future directions of research.

This work1 is concerned with basic issues of the design of calculi and proof procedures for first-order connection methods and tableaux calculi. Proof procedures for these type of calculi developed so far suffer from not exploiting proof confluence, and very often unnecessarily rely on a heavily backtrack oriented control regime.As a new result, we present a variant of a connection calculus and prove its strong completeness. This enables the design of backtrack-free contro regimes. To demonstrate that the underlying fairness condition is reasonably implementable we define an effective search strategy.

In application areas like formal software verification or in connection with lemma use, the success of automated theorem provers strongly depends on their ability to choose from a huge number of given axioms only some relevant ones. We present a new technique for deleting irrelevant clauses for model elimination proof procedures which is based on the use of abstractions. We analyze general conditions under which abstractions are well-suited for choosing useful clauses and investigate whether certain abstractions are applicable. So-called symbol abstractions are further examined in a case study which, e.g., introduces new techniques for the automatic generation of abstractions. We evaluate our techniques by means of experiments performed with the prover Setheo.

Mating search is a very general method for automating proof search; it specifies that one must find a complete mating, without specifying the way in which this is to be achieved. It is the foundation of TPS, an automated theorem-proving system for simply-typed lambda-calculus, and has proven very effective in discovering proofs of higher-order theorems. However, previous implementations of mating search have all relied on essentially the same mating search method: enumerating the paths through a matrix of literals. This is a depth-first strategy which is both computationally expensive and vulnerable to blind alleys in the search space; in addition, the incremental computation of unifiers which is required is, in the higher-order case, very inefficient. We describe a new breadth-first mating search method, called component search, in which matings are constructed by taking unions from a fixed list of smaller matings, whose unifiers are stored and manipulated as directed graphs. Component search is capable of handling much larger search spaces than were possible with path-enumeration search, and has produced fully automatic proofs of a number of interesting theorems which were previously intractable.

It has become a tradition at CADE to run a competition for first-order automated theorem provers based on the TPTP problem library. This competition (CASC) [SuSu96] aims at fully automatic ATP systems and provides various categories dedicated to diffirent problem classes of rst-order logic. The number of problems solved and the runtime is used to assess the winners in the individual categories of the competition.

Spass is an automated theorem prover for full first-order logic with equality. This system description provides a rough overview over recent developments.

Nonclassical propositional logics play an increasing role in computer science. They are used in model checking, verification, and knowledge representation. Traditional decision procedures for these logics are based on semantic tableaux [6,7,1], SAT-based methods [4], or translation into classical logic [10]. In this system abstract we overview the system K that implements the tableau method and the less traditional inverse method for propositional modal logic K.

Current programming environments for novice functional programming (FP) are inadequate. This paper describes ways of using proofs as a foundation to improve the situation, in the context of the language ML [4]. The most common way to write ML programs is via a text editor and compiler (such as the Standard ML of New Jersey compiler). But program errors, in particular type errors, are generally difficult to track down. For novices, the lack of debugging support forms a barrier to learning FP concepts [5].

An enumerative approach to conjecture formulation is presented. Its basic steps include the generation of terms and formulas, and testing the formulas in a set of models. The main procedure and some experimental results are described.

The theory of programming languages is one of the core areas of computer sci- ence offering a wealth of models and methods. Yet the complexity of most real programming languages means that a complete formalization of their semantics is only of limited use unless it is supported by mechanical means for reasoning about the formalization. This line of research started in earnest with the seminal paper by Gordon [1] who dened the semantics of a simple while-language in the HOL system and derived Hoare logic from the semantics. Since then, an ever growing number of more and more sophisticated programming languages have been embedded in theorem provers. This talk surveys some of the important developments in this area before concentrating on a specic instance, Bali. Bali (http://isabelle.in.tum.de/Bali/) is an embedding of a subset of Java in Isabelle/HOL. So far, the following aspects have been covered:

This paper presents two approaches to primitive equality treatment in higher-order (HO) automated theorem proving: a calculus EP adapting traditional first-order (FO) paramodulation [RW69], and a calculus εRUε adapting FO RUE-Resolution [Dig79] to classical type theory, i.e., HO logic based on Church’s simply typed λ-calculus. εP and εRUε extend the extensional HO resolution approach εR [BK98a]. In order to reach Henkin completeness without the need for additional extensionality axioms both calculi employ new, positive extensionality rules analogously to the respective negative ones provided by εR that operate on unification constraints. As the extensionality rules have an intrinsic and unavoidable difference-reducing character the HO paramodulation approach loses its pure term-rewriting character. On the other hand examples demonstrate that the extensionality rules harmonise quite well with the difference-reducing HO RUE-resolution idea.

P₂ is introduced: an algorithm for the automatic generation of proof search strategies from sets of examples of proofs. The proof search strategies are generated as sets of assertions (called methods) about the use of inference rules found in the examples. Sets of methods are prioritized and they can be compiled into clauses of a logic program. Proofs obtained for difficult problems in classical second-order logic are used as evidence of the adequacy of the methodology.