Lifting propositional proof compression algorithms to first-order logic

2020 ◽  
Author(s):  
Jan Gorzny ◽  
Ezequiel Postan ◽  
Bruno Woltzenlogel Paleo
Keyword(s):  
Propositional Logic ◽  
Empirical Evaluation ◽  
Order Logic ◽  
Automated Deduction ◽  
First Order Logic ◽  
Compression Algorithms ◽  
International Conference ◽  
First Order ◽  
Theorem Provers ◽  
Resolution Proofs

Abstract Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. The first approach lifted from propositional logic delays resolution with unit clauses, which are clauses that have a single literal. The second approach is partial regularization, which removes an inference $\eta $ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $\eta $ to the root of the proof. This paper describes the generalization of the algorithms LowerUnits and RecyclePivotsWithIntersection (Fontaine et al.. Compression of propositional resolution proofs via partial regularization. In Automated Deduction—CADE-23—23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31–August 5, 2011, p. 237--251. Springer, 2011) from propositional logic to first-order logic. The generalized algorithms compresses resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of these approaches is included.

scholarly journals Partial Regularization of First-Order Resolution Proofs

10.29007/3r41 ◽  
2020 ◽  
Author(s):  
Jan Gorzny ◽  
Ezequiel Postan ◽  
Bruno Woltzenlogel Paleo
Keyword(s):  
Propositional Logic ◽  
Empirical Evaluation ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Theorem Provers ◽  
Resolution Proofs

Proofs are a key feature of modern propositional and first-order theorem provers. Proofs generated by such tools serve as explanations for unsatisfiability of statements. However, these explanations are complicated by proofs which are not necessarily as concise as possible. There are a wide variety of compression techniques for propositional resolution proofs, but fewer compression techniques for first-order resolution proofs generated by automated theorem provers. This paper describes an approach to compressing first-order logic proofs based on lifting proof compression ideas used in propositional logic to first-order logic. An empirical evaluation of the approach is included.

scholarly journals Extensions in graph normal form

2020 ◽  
Author(s):  
Michał Walicki
Keyword(s):  
Normal Form ◽  
Fixed Points ◽  
Propositional Logic ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Special Cases

Abstract Graph normal form, introduced earlier for propositional logic, is shown to be a normal form also for first-order logic. It allows to view syntax of theories as digraphs, while their semantics as kernels of these digraphs. Graphs are particularly well suited for studying circularity, and we provide some general means for verifying that circular or apparently circular extensions are conservative. Traditional syntactic means of ensuring conservativity, like definitional extensions or positive occurrences guaranteeing exsitence of fixed points, emerge as special cases.

scholarly journals Checkable Proofs for First-Order Theorem Proving

10.29007/s6d1 ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Martin Suda
Keyword(s):  
Theorem Proving ◽  
Critical Mass ◽  
Current Situation ◽  
Boolean Satisfiability ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Theorem Provers ◽  
Interactive Theorem Provers ◽  
Theory Reasoning

Inspired by the success of the DRAT proof format for certification of boolean satisfiability (SAT),we argue that a similar goal of having unified automatically checkable proofs should be soughtby the developers of automated first-order theorem provers (ATPs). This would not onlyhelp to further increase assurance about the correctness of prover results,but would also be indispensable for tools which rely on ATPs,such as ``hammers'' employed within interactive theorem provers.The current situation, represented by the TSTP format is unsatisfactory,because this format does not have a standardised semantics and thus cannot be checked automatically.Providing such semantics, however, is a challenging endeavour. One would ideallylike to have a proof format which covers only-satisfiability-preserving operations such as Skolemisationand is versatile enough to encompass various proving methods (i.e. not just superposition)or is perhaps even open ended towards yet to be conceived methods or at least easily extendable in principle.Going beyond pure first-order logic to theory reasoning in the style of SMT orbeyond proofs to certification of satisfiability are further interesting challenges.Although several projects have already provided partial solutions in this direction,we would like to use the opportunity of ARCADE to further promote the idea andgather critical mass needed for its satisfactory realisation.

A First Course in Logic

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Propositional Logic ◽  
Proof Theory ◽  
Order Logic ◽  
First Order Logic ◽  
University Of Maryland ◽  
First Order ◽  
Science Philosophy ◽  
The University ◽  
Second Order Logic ◽  
Theory And Model

The ability to reason and think in a logical manner forms the basis of learning for most mathematics, computer science, philosophy and logic students. Based on the author's teaching notes at the University of Maryland and aimed at a broad audience, this text covers the fundamental topics in classical logic in an extremely clear, thorough and accurate style that is accessible to all the above. Covering propositional logic, first-order logic, and second-order logic, as well as proof theory, computability theory, and model theory, the text also contains numerous carefully graded exercises and is ideal for a first or refresher course.

Proof theory

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Propositional Logic ◽  
Completeness Theorem ◽  
Formal Proof ◽  
Order Logic ◽  
Truth Table ◽  
First Order Logic ◽  
Formal Proofs ◽  
Systematic Method ◽  
First Order

As with any logic, the semantics of first-order logic yield rules for deducing the truth of one sentence from that of another. In this chapter, we develop both formal proofs and resolution for first-order logic. As in propositional logic, each of these provides a systematic method for proving that one sentence is a consequence of another. Recall the Consequence problem for propositional logic. Given formulas F and G, the problemis to decide whether or not G is a consequence of F. From Chapter 1, we have three approaches to this problem: • We could compute the truth table for the formula F → G. If the truth values are all 1s then we conclude that F → G is a tautology and G is a consequence of F. Otherwise, G is not a consequence of F. • Using Tables 1.5 and 1.6, we could try to formally derive G from {F}. By the Completeness Theorem for propositional logic, G is a consequence of F if and only if {F} ├ G. • We could use resolution. By Theorem1.76, G is a consequence of F if and only if ∅ ∈ Res(H) where H is a formula in CNF equivalent to (F ∧￢G). Using these methods not only can we determine whether one formula is a consequence of another, but also we can determine whether a given formula is a tautology or a contradiction. A formula F is a tautology if and only if F is a consequence of (A∨￢A) if and only if ￢F is a contradiction. In this chapter, we consider the analogous problems for first-order logic. Given formulas φ and ψ, how can we determine whether ψ is a consequence of φ? Equivalently, how can we determine whether a given formula is a tautology or a contradiction? We present three methods for answering these questions. • In Section 3.1, we define a notion of formal proof for first-order logic by extending Table 1.5. • In Section 3.3, we “reduce” formulas of first-order logic to sets of formulas of propositional logic where we use resolution as defined in Chapter 1.

Structures and first-order logic

2004 ◽  
Author(s):  
Shawn Hedman
Keyword(s):  
Propositional Logic ◽  
Function Symbol ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
Ternary Relation ◽  
Specific Element ◽  
First Order ◽  
Lower Case ◽  
Second Order Logic

First-order logic is a richer language than propositional logic. Its lexicon contains not only the symbols ∧, ∨, ￢, →, and ↔ (and parentheses) from propositional logic, but also the symbols ∃ and ∀ for “there exists” and “for all,” along with various symbols to represent variables, constants, functions, and relations. These symbols are grouped into five categories. • Variables. Lower case letters from the end of the alphabet (. . . x, y, z) are used to denote variables. Variables represent arbitrary elements of an underlying set. This, in fact, is what “first-order” refers to. Variables that represent sets of elements are called second-order. Second-order logic, discussed in Chapter 9, is distinguished by the inclusion of such variables. • Constants. Lower case letters from the beginning of the alphabet (a, b, c, . . .) are usually used to denote constants. A constant represents a specific element of an underlying set. • Functions. The lower case letters f, g, and h are commonly used to denote functions. The arguments may be parenthetically listed following the function symbol as f(x1, x2, . . . , xn). First-order logic has symbols for functions of any number of variables. If f is a function of one, two, or three variables, then it is called unary, binary, or ternary, respectively. In general, a function of n variables is called n-ary and n is referred to as the arity of the function. • Relations. Capital letters, especially P, Q, R, and S, are used to denote relations. As with functions, each relation has an associated arity. We have an infinite number of each of these four types of symbols at our disposal. Since there are only finitely many letters, subscripts are used to accomplish this infinitude. For example, x1, x2, x3, . . . are often used to denote variables. Of course, we can use any symbol we want in first-order logic. Ascribing the letters of the alphabet in the above manner is a convenient convention. If you turn to a random page in this book and see “R(a, x, y),” you can safely assume that R is a ternary relation, x and y are variables, and a is a constant.

SKEPTICAL ABDUCTION

1993 ◽  
Vol 02 (04) ◽  
pp. 511-540 ◽  
Author(s):  
P. MARQUIS
Keyword(s):  
Propositional Logic ◽  
Order Logic ◽  
First Order Logic ◽  
Real Problem ◽  
Logical Framework ◽  
First Order ◽  
Selective Generation ◽  
The Given ◽  
Reasonable Prospect

Abduction is the process of generating the best explanation as to why a fact is observed given what is already known. A real problem in this area is the selective generation of hypotheses that have some reasonable prospect of being valid. In this paper, we propose the notion of skeptical abduction as a model to face this problem. Intuitively, the hypotheses pointed out by skeptical abduction are all the explanations that are consistent with the given knowledge and that are minimal, i.e. not unnecessarily general. Our contribution is twofold. First, we present a formal characterization of skeptical abduction in a logical framework. On this ground, we address the problem of mechanizing skeptical abduction. A new method to compute minimal and consistent hypotheses in propositional logic is put forward. The extent to which skeptical abduction can be mechanized in first—order logic is also investigated. In particular, two classes of first-order formulas in which skeptical abduction is effective are provided. As an illustration, we finally sketch how our notion of skeptical abduction applies as a theoretical tool to some artificial intelligence problems (e.g. diagnosis, machine learning).

scholarly journals SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS

2010 ◽  
Vol 3 (2) ◽  
pp. 175-227 ◽  
Author(s):  
PETER MILNE
Keyword(s):  
Propositional Logic ◽  
Natural Deduction ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Models ◽  
Careful Attention ◽  
Classical Propositional Logic ◽  
First Order ◽  
Invalid Inference ◽  
Subformula Property

Various natural deduction formulations of classical, minimal, intuitionist, and intermediate propositional and first-order logics are presented and investigated with respect to satisfaction of the separation and subformula properties. The technique employed is, for the most part, semantic, based on general versions of the Lindenbaum and Lindenbaum–Henkin constructions. Careful attention is paid (i) to which properties of theories result in the presence of which rules of inference, and (ii) to restrictions on the sets of formulas to which the rules may be employed, restrictions determined by the formulas occurring as premises and conclusion of the invalid inference for which a counterexample is to be constructed. We obtain an elegant formulation of classical propositional logic with the subformula property and a singularly inelegant formulation of classical first-order logic with the subformula property, the latter, unfortunately, not a product of the strategy otherwise used throughout the article. Along the way, we arrive at an optimal strengthening of the subformula results for classical first-order logic obtained as consequences of normalization theorems by Dag Prawitz and Gunnar Stålmarck.

Sign in / Sign up

Export Citation Format

Share Document