Optimal Axiomatizations of Finitely Valued Logics

We investigate the problem of finding optimal axiomatizations for operators and distribution quantifiers in finitely valued first-order logics. We show that the problem can be viewed as the minimization of certain propositional formulas. We outline a general procedure leading to optimized operator and quantifier rules for the sequent calculus, for natural deduction, and for clause formation. The main tools are variants of two-valued and many-valued propositional resolution, as well as a novel rule called combination. In the case of operators and quantifiers based on semilattices, rules with a minimal branching degree can be obtained by instantiating a schema, which can also be used for optimal tableaux with sets-as-signs.     

Short proofs for tricky formulas

Summary The object of this paper is to demonstrate how certain tricky mathematical arguments can be encoded as short formal proofs for the propositional tautologies representing the mathematical statements. Using resolution as a base proof system for the propositional calculus, we exhibit these short proofs under resolution augmented by one of two principles: the principle of extension, originally suggested by Tseitin, and the principle of symmetry, introduced in this paper. These short proofs illustrate the power of extension and symmetry in theorem proving.The principle of extension allows the introduction of auxiliary variables to represent intermediate formulas so that the length of a proof can be significantly reduced by manipulating these variables instead of the formulas that they stand for. Symmetry, on the other hand, allows one to recognize that a tautology remains invariant under certain permutations of variable names, and use that information to avoid repeated independent derivations of intermediate formulas that are merely permutational variants of one another.First we show that a number of inductive arguments can be encoded as short formal proofs using either extension or symmetry. We provide the details for the tautologies derived by encoding the statement, An acyclic digraph on n vertices must have a source. We then consider the familiar checkerboard puzzle which asserts that a checkerboard, two of whose diagonally opposite corner squares are removed, cannot be perfectly covered with dominoes. We demonstrate short proofs for the tautologies derived from the above assertion, using extension to mimic the tricky informal argument. Finally, we consider statements asserting the Ramsey property of numbers much larger than the critical Ramsey numbers. We show that the proof of Ramsey's theorem can be imitated using the principle of symmetry to yield short proofs for these tautologies.The main theme of the paper is that both extension and symmetry are very powerful augmentations to resolution. We leave open whether either extension or symmetry can polynomially simulate the other.This work was performed while the author was with the General Electric Research Center     

Algebraic proofs over noncommutative formulas

We study possible formulations of algebraic propositional proof systems operating with noncommutative formulas. We observe that a simple formulation gives rise to systems at least as strong as Frege, yielding a semantic way to define a Cook-Reckhow (i.e., polynomially verifiable) algebraic analog of Frege proofs, different from that given in Buss et al. (1997) and Grigoriev and Hirsch (2003). We then turn to an apparently weaker system, namely, polynomial calculus (PC) where polynomials are written as ordered formulas (PC over ordered formulas, for short). Given some fixed linear order on variables, an arithmetic formula is ordered if for each of its product gates the left subformula contains only variables that are less-than or equal, according to the linear order, than the variables in the right subformula of the gate. We show that PC over ordered formulas (when the base field is of zero characteristic) is strictly stronger than resolution, polynomial calculus and polynomial calculus with resolution (PCR), and admits polynomial-size refutations for the pigeonhole principle and Tseitin?s formulas. We conclude by proposing an approach for establishing lower bounds on PC over ordered formulas proofs, and related systems, based on properties of lower bounds on noncommutative formulas (Nisan, 1991).The motivation behind this work is developing techniques incorporating rank arguments (similar to those used in arithmetic circuit complexity) for establishing lower bounds on propositional proofs.     

Using linear algebra in decomposition of Farkas interpolants

The use of propositional logic and systems of linear inequalities over reals is a common means to model software for formal verification. Craig interpolants constitute a central building block in this setting for over-approximating reachable states, e.g. as candidates for inductive loop invariants. Interpolants for a linear system can be efficiently computed from a Simplex refutation by applying the Farkas’ lemma. However, these interpolants do not always suit the verification task—in the worst case, they can even prevent the verification algorithm from converging. This work introduces the decomposed interpolants, a fundamental extension of the Farkas interpolants, obtained by identifying and separating independent components from the interpolant structure, using methods from linear algebra. We also present an efficient polynomial algorithm to compute decomposed interpolants and analyse its properties. We experimentally show that the use of decomposed interpolants in model checking results in immediate convergence on instances where state-of-the-art approaches diverge. Moreover, since being based on the efficient Simplex method, the approach is very competitive in general.

     

Formalization of the Resolution Calculus for First-Order Logic

I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations and semantic trees. The correspondence between unsatisfiable sets of clauses and finite semantic trees is formalized in Herbrand’s theorem. I discuss the difficulties that I had formalizing proofs of the lifting lemma found in the literature, and I formalize a correct proof. The completeness proof is by induction on the size of a finite semantic tree. Throughout the paper I emphasize details that are often glossed over in paper proofs. I give a thorough overview of formalizations of first-order logic found in the literature. The formalization of resolution is part of the IsaFoL project, which is an effort to formalize logics in Isabelle/HOL.     

Resolution proof transformation for compression and interpolation

Verification methods based on SAT, SMT, and theorem proving often rely on proofs of unsatisfiability as a powerful tool to extract information in order to reduce the overall effort. For example a proof may be traversed to identify a minimal reason that led to unsatisfiability, for computing abstractions, or for deriving Craig interpolants. In this paper we focus on two important aspects that concern efficient handling of proofs of unsatisfiability: compression and manipulation. First of all, since the proof size can be very large in general (exponential in the size of the input problem), it is indeed beneficial to adopt techniques to compress it for further processing. Secondly, proofs can be manipulated as a flexible preprocessing step in preparation for interpolant computation. Both these techniques are implemented in a framework that makes use of local rewriting rules to transform the proofs. We show that a careful use of the rules, combined with existing algorithms, can result in an effective simplification of the original proofs. We have evaluated several heuristics on a wide range of unsatisfiable problems deriving from SAT and SMT test cases.     

Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems

We describe a complete theorem proving procedure for higher-order logic that uses SAT-solving to do much of the heavy lifting. The theoretical basis for the procedure is a complete, cut-free, ground refutation calculus that incorporates a restriction on instantiations. The refined nature of the calculus makes it conceivable that one can search in the ground calculus itself, obtaining a complete procedure without resorting to meta-variables and a higher-order lifting lemma. Once one commits to searching in a ground calculus, a natural next step is to consider ground formulas as propositional literals and the rules of the calculus as propositional clauses relating the literals. With this view in mind, we describe a theorem proving procedure that primarily generates relevant formulas along with their corresponding propositional clauses. The procedure terminates when the set of propositional clauses is unsatisfiable. We prove soundness and completeness of the procedure. The procedure has been implemented in a new higher-order theorem prover, Satallax, which makes use of the SAT-solver MiniSat. We also describe the implementation and give several examples. Finally, we include experimental results of Satallax on the higher-order part of the TPTP library.     

命题逻辑提升到一阶逻辑上的子句消去方法

在基于命题逻辑的可满足性问题（SAT）求解器和基于一阶逻辑的定理证明器上，子句集简化一直是必不可少的步骤，而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分。将命题逻辑中的子句消去方法归结隐藏恒真消去方法（RHTE）和归结隐藏包含消去方法（RHSE）提升到一阶逻辑上，并且利用蕴含模归结原则（IMR）证明了这种提升方式在一阶逻辑上具有可靠性（Soundness），即依据这两种子句消去方法删除一阶逻辑公式集中的子句，并不会改变公式集的可满足性或者不可满足性。此外，将这两个方法与一阶逻辑子句消去方法锁子句消去方法（BCE）和归结包含消去方法（RSE）进行组合推广，发展得到一阶逻辑上新型子句消去方法（BC+RHS）E、（RS+RHT）E和（RHS+RHT）E，并且证明了这3种子句消去方法在一阶逻辑上的可靠性。最后，分析比较了这些子句消去方法的有效性，并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性。     

Davis-Putnam resolution versus unrestricted resolution

A resolution proof of an unsatisfiable propositional formula in conjunctive normal form is a Davis-Putnam resolution proof iff there exists a sequence of the variables of the formula such thatx is eliminated (with the resolution rule) beforey on any branch of the proof tree representing the resolution proof, only ifx is beforey in this sequence. Davis-Putnam resolution is one of several resolution restrictions. It is complete.We present an infinite family of unsatisfiable propositional formulas and show: These formulas have unrestricted resolution proofs whose length is polynomial in their size. All Davis-Putnam resolution proofs of these formulas are of superpolynomial length. In the terminology of [4, definition 1.5]: Davis-Putnam resolution does notp-simulate unrestricted resolution.     

Consequence finding and computing answers with defaults

Consequence finding has been recognized as an important technique in many intelligent systems involving inference. In previous work, propositional or first-order clausal theories have been considered for consequence finding. In this paper, we consider consequence finding from a default theory, which consists of a first-order clausal theory and a set of normal defaults. In an extension of a default theory, consequence finding can be done with the generating defaults for the extension. Alternatively, all extensions can be represented at once with the conditional answer format, which represents how a conclusion depends on which defaults. We also propose a procedure for consequence finding and query answering in a default theory using the first-order consequence-finding procedure SOL. In computing consequences from default theories efficiently, the notion of TCS-freeness is most important to prune a large number of irrational tableaux induced by the generating defaults for an extension. In order to simulate the TCS-freeness, the refined SOL calculus called SOL-S(Γ) is adopted using skip preference and complement checking. This research is supported in part by JSPS Grant-in-Aid for Scientific Research (No. 17300051)     

Constraint solving for interpolation

Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing the separation between the sets of ‘good’ and ‘bad’ states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in a black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.     

Data Compression for Proof Replay

We describe a compressing translation from SAT solver generated propositional resolution refutation proofs to classical natural deduction proofs. The resulting proof can usually be checked quicker than one that simply simulates the original resolution proof. We use this result in interactive theorem provers, to speed up reconstruction of SAT solver generated proofs. The translation is fast and scales up to large proofs with millions of inferences.     

The map and blend scattered data interpolant on a sphere

The map and blend technique constructs a function defined over the sphere that interpolates to a discrete sample of measurements at arbitrary locations on the sphere. This technique consists of two different mappings of the sphere to planar domains, solving two corresponding scattered data interpolation problems on the planar domains, and then the interpolant on the sphere is formed by blending these two planar interpolants. If the user has software for solving the scattered data interpolation problem on a planar domain, only a small programming effort is needed to implement the map and blend interpolant on the sphere. Although any interpolant to scattered data on a planar domain can be used in our general technique, we use the multiquadric radial basis method.     

MAX^＋公式的结构特征

改名是一个将变元映射到变元本身或它的补的函数,变元改名是公式变元集合上的一个置换,文字改名是一个改名和一个变元改名的组合。改名技术在简化一些难例公式的消解证明和构造高效的可满足算法方面有重要意义。MAX^＋公式是MU公式中的一个重要子类,该类公式可以通过递归的方式产生。通过分析MAX^＋公式的结构,得到了一些关于此类公式的结构特点,对进一步研究这类公式的改名问题有较大意义。     

Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems

We prove a dichotomy theorem for the rank of propositional contradictions, uniformly generated from first-order sentences, in both the Lovász-Schrijver (LS) and Sherali-Adams (SA) refutation systems. More precisely, we first show that the propositional translations of first-order formulae that are universally false, that is, fail in all finite and infinite models, have LS proofs whose rank is constant, independent of the size of the (finite) universe. In contrast to that, we prove that the propositional formulae that fail in all finite models, but hold in some infinite structure, require proofs whose SA rank grows polynomially with the size of the universe. Until now, this kind of so-called complexity gap theorem has been known for tree-like Resolution and, in somehow restricted forms, for the Resolution and Nullstellensatz systems. As far as we are aware, this is the first time the Sherali-Adams lift-and-project method has been considered as a propositional refutation system (since the conference version of this paper, SA has been considered as a refutation system in several further papers). An interesting feature of the SA system is that it simulates LS, the Lovász-Schrijver refutation system without semi-definite cuts, in a rank-preserving fashion.     

Parameterized Proof Complexity

We propose a proof-theoretic approach for gaining evidence that certain parameterized problems are not fixed-parameter tractable. We consider proofs that witness that a given propositional formula cannot be satisfied by a truth assignment that sets at most k variables to true, considering k as the parameter (we call such a formula a parameterized contradiction). One could separate the parameterized complexity classes FPT and W[SAT] by showing that there is no fpt-bounded parameterized proof system for parameterized contradictions, i.e., that there is no proof system that admits proofs of size f(k)n ^O(1) where f is a computable function and n represents the size of the propositional formula. By way of a first step, we introduce the system of parameterized tree-like resolution and show that this system is not fpt-bounded. Indeed, we give a general result on the size of shortest tree-like resolution proofs of parameterized contradictions that uniformly encode first-order principles over a universe of size n. We establish a dichotomy theorem that splits the exponential case of Riis’s complexity gap theorem into two subcases, one that admits proofs of size f(k)n ^O(1) and one that does not. We also discuss how the set of parameterized contradictions may be embedded into the set of (ordinary) contradictions by the addition of new axioms. When embedded into general (DAG-like) resolution, we demonstrate that the pigeonhole principle has a proof of size 2 ^k n ². This contrasts with the case of tree-like resolution where the embedded pigeonhole principle falls into the “non-FPT” category of our dichotomy.     

Adding equality to semantic tableaux

An extension to the system of semantic tableaux to deal with first-order logic with equality is introduced and proved sound and complete. This involves the use of partial unification, an operation which is based on unification without the presence of variables. We show, further, that semantic tableaux with partial unification provide a sound and complete proof method without needing the functionally reflexive axioms. We also give an example of an ordering rule which allows us to provide less complex proofs in the ground case.     

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.     

Many-valued logic and mixed integer programming

We generalize prepositional semantic tableaux for classical and many-valued logics toconstraint tableaux. We show that this technique is a generalization of the standard translation from CNF formulas into integer programming. The main advantages are (i) a relatively efficient satisfiability checking procedure for classical, finitely-valued and, for the first time, for a wide range of infinitely-valued propositional logics; (ii) easy NP-containment proofs for many-valued logics. The standard translation of two-valued CNF formulas into integer programs and Tseitin's structure preserving clause form translation are obtained as a special case of our approach.Part of the research reported here was carried out while the author was supported by a grant within the DFG Schwerpunktprogramm Deduktion. Preliminary and partial versions of this paper were published as [15, 16].     

Clausal Presentation of Theories in Deduction Modulo

Resolution modulo is an extension of first-order resolution in which rewrite rules are used to rewrite clauses during the search. In the first version of this method, clauses are rewritten to arbitrary propositions. These propositions are needed to be dynamically transformed into clauses. This unpleasant feature can be eliminated when the rewrite system is clausal, i.e., when it rewrites clauses to clauses. We show in this paper how to transform any rewrite system into a clausal one, preserving the existence of cut free proofs of any sequent.