Eliminating duplication with the hyper-linking strategy

The efficiency of almost all theorem proving methods suffers from a phenomenon called duplication of instances of clauses. In this paper, we present a novel technique, called the hyper-linking strategy, to eliminate such duplication. This strategy is complete for the full first-order predicate calculus. We show the effectiveness of this strategy by comparing it with other proving methods. We give empirical evidence that both the Davis-Putnam procedure and the hyper-linking strategy are comparable to each other and better than other common theorem proving strategies on propositional calculus problems. The fact that the Davis-Putnam procedure is faster than resolution and other common methods on propositional problems seems not to be appreciated by a large segment of the theorem proving community. Also, we give empirical evidence that the hyper-linking strategy is better than other common theorem proving methods on near-propositional problems like logic puzzles. We attempt to explain the superior behavior of the hyper-linking strategy and the Davis-Putnam procedure by examining the kinds of duplication that can occur during the search with the different methods. In addition, we show the completeness of the hyper-linking strategy combined with several support strategies.This research was partially supported by NSF under grant CCR-8802282.     

A simplified problem reduction format

Some new approaches to mechanical theorem proving in the first-order predicate calculus are presented. These are based on a natural deduction system which can be used to show that a set of clauses is inconsistent. This natural deduction system distinguishes positive from negative literals and treats clauses having 0, 1, and 2 or more positive literals in three separate ways. Several such systems are presented. The systems are complete and relatively simple and allow a goal to be decomposed into subgoals, and solutions to the subgoals can then be searched for in the same way. Also, the systems permit a natural use of semantic information to delete unachievable subgoals. The goal-subgoal structure of these systems should allow much of the current artificial intelligence methodology to be applied to mechanical theorem proving.     

SMELS: Satisfiability Modulo Equality with Lazy Superposition

We consider the problem of checking satisfiability of quantified formulae in First Order Logic with Equality. We propose a new procedure for combining SAT solvers with Superposition Theorem Provers to handle quantified formulae in an efficient and complete way. In our procedure, the input formula is converted into CNF as in traditional first order logic theorem provers. The ground clauses are given to the SAT solver, which runs a DPLL method to build partial models. The partial model is reduced, and then passed to a Superposition procedure, along with justifications of literals. The Superposition procedure then performs an inference rule, which we call Justified Superposition, between the ground literals and the nonground clauses, plus usual Superposition rules with the nonground clauses. Any resulting ground clauses are provided to the DPLL engine. We prove the completeness of our procedure, using a nontrivial modification of the Bachmair and Ganzinger’s model generation technique. We have implemented a theorem prover based on this idea by reusing state-of-the-art SAT solver and Superposition Theorem Prover. Our theorem prover inherits the best of both worlds: a SAT solver to handle ground clauses efficiently, and a Superposition theorem prover which uses powerful orderings to handle the nonground clauses. Experimental results are promising, and hereby confirm the viability of our method.     

Deciding Effectively Propositional Logic Using DPLL and Substitution Sets

We introduce a DPLL calculus that is a decision procedure for the Bernays-Schönfinkel class, also known as EPR. Our calculus allows combining techniques for efficient propositional search with data-structures, such as Binary Decision Diagrams, that can efficiently and succinctly encode finite sets of substitutions and operations on these. In the calculus, clauses comprise of a sequence of literals together with a finite set of substitutions; truth assignments are also represented using substitution sets. The calculus works directly at the level of sets, and admits performing simultaneous constraint propagation and decisions, resulting in potentially exponential speedups over existing approaches.     

The semantics of answer literals

We describe a semantics for answer literals that is not tied to the specific detaisl of the resolution proof procedure. We also describe a number of applications of answer literals to mathematical theorem proving.Author supported by NSF Grant CCR-9503445.     

Analytic Tableaux for Higher-Order Logic with Choice

While many higher-order interactive theorem provers include a choice operator, higher-order automated theorem provers so far have not. In order to support automated reasoning in the presence of a choice operator, we present a cut-free ground tableau calculus for Church’s simple type theory with choice. The tableau calculus is designed with automated search in mind. In particular, the rules only operate on the top level structure of formulas. Additionally, we restrict the instantiation terms for quantifiers to a universe that depends on the current branch. At base types the universe of instantiations is finite. Both of these restrictions are intended to minimize the number of rules a corresponding search procedure is obligated to consider. We prove completeness of the tableau calculus relative to Henkin models.     

余式方法中的线性策略以及语义策略和锁策略

本文证明了一介定性证明的余式方法对于线性策略是完备的，而对于语义策略和锁策略，在例题演算中是完备的，在一阶谓词演算法，对于一种较弱形式的语义策略和锁策略，提完备的。     

A simplifier for propositional formulas with many binary clauses

Deciding whether a propositional formula in conjunctive normal form is satisfiable (SAT) is an NP-complete problem. The problem becomes linear when the formula contains binary clauses only. Interestingly, the reduction to SAT of a number of well-known and important problems--such as classical AI planning and automatic test pattern generation for circuits--yields formulas containing many binary clauses. In this paper we introduce and experiment with 2-SIMPLIFY, a formula simplifier targeted at such problems. 2-SIMPLIFY constructs the transitive closure of the implication graph corresponding to the binary clauses in the formula and uses this graph to deduce new unit literals. The deduced literals are used to simplify the formula and update the graph, and so on, until stabilization. Finally, we use the graph to construct an equivalent, simpler set of binary clauses. Experimental evaluation of this simplifier on a number of bench-mark formulas produced by encoding AI planning problems prove 2-SIMPLIFY to be a useful tool in many circumstances.     

Craig Interpolation with Clausal First-Order Tableaux

We develop foundations for computing Craig-Lyndon interpolants of two given formulas with first-order theorem provers that construct clausal tableaux. Provers that can be understood in this way include efficient machine-oriented systems based on calculi of two families: goal-oriented such as model elimination and the connection method, and bottom-up such as the hypertableau calculus. We present the first interpolation method for first-order proofs represented by closed tableaux that proceeds in two stages, similar to known interpolation methods for resolution proofs. The first stage is an induction on the tableau structure, which is sufficient to compute propositional interpolants. We show that this can linearly simulate different prominent propositional interpolation methods that operate by an induction on a resolution deduction tree. In the second stage, interpolant lifting, quantified variables that replace certain terms (constants and compound terms) by variables are introduced. We justify the correctness of interpolant lifting (for the case without built-in equality) abstractly on the basis of Herbrand’s theorem and for a different characterization of the formulas to be lifted than in the literature. In addition, we discuss various subtle aspects that are relevant for the investigation and practical realization of first-order interpolation based on clausal tableaux.

     

Implementing the Davis–Putnam Method

The method proposed by Davis, Putnam, Logemann, and Loveland for propositional reasoning, often referred to as the Davis–Putnam method, is one of the major practical methods for the satisfiability (SAT) problem of propositional logic. We show how to implement the Davis–Putnam method efficiently using the trie data structure for propositional clauses. A new technique of indexing only the first and last literals of clauses yields a unit propagation procedure whose complexity is sublinear to the number of occurrences of the variable in the input. We also show that the Davis–Putnam method can work better when unit subsumption is not used. We illustrate the performance of our programs on some quasigroup problems. The efficiency of our programs has enabled us to solve some open quasigroup problems.     

Comments on “tautology testing with a generalized matrix reduction method”

Bibel [1] has given a proof system for the propositional calculus called (generalized) matrix reduction. When matrix splitting is restricted to one literal at a time the system is the same as Galil's system [2] of enumeration dags. In fact the relation is even closer. The matrices produced by the reduction on a set of literals {I} are exactly the set of clauses appearing on a dag after |I| consecutive branches with substitute for the same literals. The clauses M₁ (which do not appear in the matrices M^c) are exactly the clauses whose branches close with the empty clause Λ. Thus the saving in space is at most by a factor of |I|, but |I| is bounded from above by log₂M to ‘guarantee polynomial behaviour’. Hence Galil's system polynomially simulates matrix reduction and thus matrix reduction is also an exponential proof procedure.     

Combining SAT Methods with Non-Clausal Decision Heuristics

A decision procedure for arbitrary first-order formulas can be viewed as combining a propositional search with a decision procedure for conjunctions of first-order literals, so Boolean SAT methods can be used for the propositional search in order to improve the performance of the overall decision procedure. We show how to combine some Boolean SAT methods with non-clausal heuristics developed for first-order decision procedures. The combination of methods leads to a smaller number of decisions than either method alone.     

RRTP - A Replacement Rule Theorem Prover

The Replacement Rule Theorem Prover (RRTP) is an instance-based, refutational, first-order clausal theorem prover. The prover is motivated by the idea of selectively replacing predicates by their definitions, and operates by selecting relevant instances of the input clauses. The relevant instances are grounded, if necessary, and tested for unsatisfiability by using a fast propositional calculus decision procedure.     

Theorem Proving Modulo

Deduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate computations and deductions in a clean way. The first contribution of this paper is to define a sequent calculus modulo that gives a proof-theoretic account of the combination of computations and deductions. The congruence on propositions is handled through rewrite rules and equational axioms. Rewrite rules apply to terms but also directly to atomic propositions. The second contribution is to give a complete proof search method, called extended narrowing and resolution (ENAR), for theorem proving modulo such congruences. The completeness of this method is proved with respect to provability in sequent calculus modulo. An important application is that higher-order logic can be presented as a theory in deduction modulo. Applying the ENAR method to this presentation of higher-order logic subsumes full higher-order resolution. This revised version was published online in August 2006 with corrections to the Cover Date.     

A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs

Combinatorial proofs are abstract invariants for sequent calculus proofs, similarly to homotopy groups which are abstract invariants for topological spaces. Sequent calculus fails to be surjective onto combinatorial proofs, and here we extract a syntactically motivated closure of sequent calculus from which there is a surjection onto a complete set of combinatorial proofs. We characterize a class of canonical sequent calculus proofs for the full set of propositional tautologies and derive a new completeness theorem for combinatorial propositions. For this, we define a new mapping between combinatorial proofs and sequent calculus proofs, different from the one originally proposed, which explicitly links the logical flow graph of a proof to a skew fibration between graphs of formulas. The categorical properties relating the original and the new mappings are explicitly discussed.     

Theorem proving with abstraction

A class of mappings called abstractions are defined, and examples of abstractions are given. These functions map a set S of clauses onto a possibly simpler set T of clauses. Also, resolution proofs from S map onto possibly simpler resolution proofs from T. In order to search for a proof of a clause C from S, it suffices to search for a proof from T and attempt to invert the abstraction mapping to obtain a proof of C from S. Some theorem proving strategies based on this idea are presented. Most of these strategies are complete. A method of using more than one abstraction at the same time is also presented. This requires the use of ‘multiclauses’, which are multisets of literals, and associated ‘m-abstraction mappings’ on multiclauses. Certain abstractions are especially interesting, because they correspond to particular interpretations of the set S of clauses. The use of abstractions permits the advantages of set-of-support strategies to be realized in arbitrary complete non set-of-support resolution strategies.     

Answering Queries Addressed to Several Databases According to a Majority Merging Approach

The general context of this work is the problem of merging data provided by several sources which can be contradictory. Focusing on the case when the information sources do not contain any disjunction, this paper first defines a propositional modal logic for reasoning with data obtained by merging several information sources according to a majority approach. Then it defines a theorem prover to automatically deduce these merged data. Finally, it shows how to use this prover to implement a query evaluator which answers queries addressed to several databases. This evaluator is such that the answer to a query is the one that could be computed by a classical evaluator if the query was addressed to the merged databases. The databases we consider are made of an extensional part, i.e. a set of positive or negative ground literals, and an intensional part i.e. a set of first order function-free clauses. A restriction is imposed to these databases in order to avoid disjunctive data.     

CLIN-S - A Semantically Guided First-Order Theorem Prover

CLIN-S is an instance-based, clause-form first-order theorem prover. CLIN-S employs three inference procedures: semantic hyper-linking, which uses semantics to guide the proof search and performs well on non-Horn parts of the proofs involving small literals, rough resolution, which removes large literals in the proofs, and UR resolution, which proves the Horn parts of the proofs. A semantic structure for the input clauses is given as input. During the search for the proof, ground instances of the input clauses are generated and new semantic structures are built based on the input semantics and a model of the ground clause set. A proof is found if the ground clause set is unsatisfiable. In this article, we describe the system architecture and major inference rules used in CLIN-S.     

A Disjunctive Positive Refinement of Model Elimination and its Application to Subsumption Deletion

The Model Elimination (ME) calculus is a refutationally complete,goal-oriented calculus for first-order clause logic. In this article, weintroduce a new variant called disjunctive positive ME (DPME); it improveson Plaisteds positive refinement of ME in that reduction steps areallowed only with positive literals stemming from clauses having at leasttwo positive literals (so-called disjunctive clauses). DPME is motivated byits application to various kinds of subsumption deletion: in order to applysubsumption deletion in ME equally successful as in resolution, it iscrucial to employ a version of ME that minimizes ancestor context (i.e., thenecessary A-literals to find a refutation). DPME meets this demand. Wedescribe several variants of ME with subsumption, the most important onesbeing ME with backward and forward subsumption and theT*-Context Check. We compare their pruning power, also takinginto consideration the well-known regularity restriction. All proofs aresupplied. The practicability of our approach is demonstrated with experiments.