scholarly journals SGGS Theorem Proving: an Exposition

10.29007/m2vf ◽  
2018 ◽  
Author(s):  
Maria Paola Bonacina ◽  
David Plaisted
Keyword(s):  
Theorem Proving ◽  
Order Logic ◽  
First Order Logic ◽  
Candidate Model ◽  
Narrative Style ◽  
First Order ◽  
The Core ◽  
Theorem Provers ◽  
Instance Generation ◽  
Main Ideas

We present in expository style the main ideas in SGGS, which stands for Semantically-Guided Goal-Sensitive theorem proving. SGGS uses sequences of constrained clauses to represent models, instance generation to go from a candidate model to the next, and resolution as well as other inferences to repair the model. SGGS is refutationally complete for first-order logic, DPLL-style model based, semantically guided, goal sensitive, and proof confluent, which appears to be a rare combination of features. In this paper we describe the core of SGGS in a narrative style, emphasizing ideas and trying to keep technicalities to a minimum, in order to advertise it to builders and users of theorem provers.

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.

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 Formalization of Linear Space Theory in the Higher-Order Logic Proving System

2013 ◽  
Vol 2013 ◽  
pp. 1-6 ◽  
Author(s):  
Jie Zhang ◽  
Danwen Mao ◽  
Yong Guan
Keyword(s):  
Linear Space ◽  
Theorem Proving ◽  
Predicate Logic ◽  
Higher Order ◽  
Order Logic ◽  
First Order Logic ◽  
Space Theory ◽  
Higher Order Logic ◽  
First Order ◽  
Important Approach

Theorem proving is an important approach in formal verification. Higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and stronger semantics. Higher-order logic is more expressive. This paper presents the formalization of the linear space theory in HOL4. A set of properties is characterized in HOL4. This result is used to build the underpinnings for the application of higher-order logic in a wider spectrum of engineering applications.

scholarly journals Different Proofs are Good Proofs

10.29007/kwk9 ◽  
2018 ◽  
Author(s):  
Geoff Sutcliffe ◽  
Cynthia Chang ◽  
Li Ding ◽  
Deborah McGuinness ◽  
Paulo Pinheiro da Silva
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Problem Library

In order to compare the quality of proofs, it is necessary to measure artifacts of the proofs, and evaluate the measurements to determine differences between the proofs. This paper discounts the approach of ranking measurements of proof artifacts, and takes the position that different proofs are good proofs. The position is based on proofs in the TSTP solution library, which are generated by Automated Theorem Proving (ATP) systems applied to first-order logic problems in the TPTP problem library.

scholarly journals Subformula Linking for Intuitionistic Logic with Application to Type Theory

2021 ◽  
pp. 200-216
Author(s):  
Kaustuv Chaudhuri
Keyword(s):  
Theorem Proving ◽  
Intuitionistic Logic ◽  
Type Theory ◽  
Linear Logic ◽  
Interactive Theorem Proving ◽  
Order Logic ◽  
First Order Logic ◽  
Direct Manipulation ◽  
First Order

AbstractSubformula linking is an interactive theorem proving technique that was initially proposed for (classical) linear logic. It is based on truth and context preserving rewrites of a conjecture that are triggered by a user indicating links between subformulas, which can be done by direct manipulation, without the need of tactics or proof languages. The system guarantees that a true conjecture can always be rewritten to a known, usually trivial, theorem. In this work, we extend subformula linking to intuitionistic first-order logic with simply typed lambda-terms as the term language of this logic. We then use a well known embedding of intuitionistic type theory into this logic to demonstrate one way to extend linking to type theory.

Sign in / Sign up

Export Citation Format

Share Document