-
Partial Regularization of First-Order Resolution Proofs
Authors:
Jan Gorzny,
Ezequiel Postan,
Bruno Woltzenlogel Paleo
Abstract:
Resolution and superposition are common techniques which have seen widespread use with propositional and first-order logic in modern theorem provers. In these cases, resolution proof production is a key feature of such tools; however, the proofs that they produce are not necessarily as concise as possible. For propositional resolution proofs, there are a wide variety of proof compression technique…
▽ More
Resolution and superposition are common techniques which have seen widespread use with propositional and first-order logic in modern theorem provers. In these cases, resolution proof production is a key feature of such tools; however, the proofs that they produce are not necessarily as concise as possible. For propositional resolution proofs, there are a wide variety of proof compression techniques. There are fewer techniques for compressing 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. One method for propositional proof compression is partial regularization, which removes an inference $η$ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference in every path from $η$ to the root of the proof. This paper describes the generalization of the partial-regularization algorithm RecyclePivotsWithIntersection [10] from propositional logic to first-order logic. The generalized algorithm performs partial regularization of resolution proofs containing resolution and factoring inferences with unification. An empirical evaluation of the generalized algorithm and its combinations with the previously lifted GreedyLinearFirstOrderLowerUnits algorithm [12] is also presented
△ Less
Submitted 17 April, 2018;
originally announced April 2018.
-
Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving
Authors:
Catherine Dubois,
Bruno Woltzenlogel Paleo
Abstract:
This volume of EPTCS contains the proceedings of the Fifth Workshop on Proof Exchange for Theorem Proving (PxTP 2017), held on September 23-24, 2017 as part of the Tableaux, FroCoS and ITP conferences in Brasilia, Brazil. The PxTP workshop series brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms, with a sp…
▽ More
This volume of EPTCS contains the proceedings of the Fifth Workshop on Proof Exchange for Theorem Proving (PxTP 2017), held on September 23-24, 2017 as part of the Tableaux, FroCoS and ITP conferences in Brasilia, Brazil. The PxTP workshop series brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms, with a special focus on proofs. The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation between such tools in larger systems has demonstrated the potential to reduce the amount of manual intervention. Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop series strives to encourage such cooperation by inviting contributions on all aspects of cooperation between reasoning tools, whether automatic or interactive.
△ Less
Submitted 3 December, 2017;
originally announced December 2017.
-
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution
Authors:
Daniyar Itegulov,
John Slaney,
Bruno Woltzenlogel Paleo
Abstract:
This paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of)…
▽ More
This paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.
△ Less
Submitted 31 October, 2017; v1 submitted 11 April, 2017;
originally announced April 2017.
-
An Expressive Probabilistic Temporal Logic
Authors:
Bruno Woltzenlogel Paleo
Abstract:
This paper argues that a combined treatment of probabilities, time and actions is essential for an appropriate logical account of the notion of probability; and, based on this intuition, describes an expressive probabilistic temporal logic for reasoning about actions with uncertain outcomes. The logic is modal and higher-order: modalities annotated by actions are used to express possibility and ne…
▽ More
This paper argues that a combined treatment of probabilities, time and actions is essential for an appropriate logical account of the notion of probability; and, based on this intuition, describes an expressive probabilistic temporal logic for reasoning about actions with uncertain outcomes. The logic is modal and higher-order: modalities annotated by actions are used to express possibility and necessity of propositions in the next states resulting from the actions, and a higher-order function is needed to express the probability operator. The proposed logic is shown to be an adequate extension of classical mathematical probability theory, and its expressiveness is illustrated through the formalization of the Monty Hall problem.
△ Less
Submitted 7 October, 2017; v1 submitted 24 March, 2016;
originally announced March 2016.
-
Conflict Resolution: a First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning
Authors:
John Slaney,
Bruno Woltzenlogel Paleo
Abstract:
This paper defines the (first-order) conflict resolution calculus: an extension of the resolution calculus inspired by techniques used in modern SAT-solvers. The resolution inference is restricted to (first-order) unit-propagation and the calculus is extended with a mechanism for assuming decision literals and a new inference rule for clause learning, which is a first-order generalization of the p…
▽ More
This paper defines the (first-order) conflict resolution calculus: an extension of the resolution calculus inspired by techniques used in modern SAT-solvers. The resolution inference is restricted to (first-order) unit-propagation and the calculus is extended with a mechanism for assuming decision literals and a new inference rule for clause learning, which is a first-order generalization of the propositional conflict-driven clause learning (CDCL) procedure. The calculus is sound (because it can be simulated by natural deduction) and refutationally complete (because it can simulate resolution), and these facts are proven in detail here.
△ Less
Submitted 15 February, 2016;
originally announced February 2016.
-
Proceedings Eleventh Workshop on User Interfaces for Theorem Provers
Authors:
Christoph Benzmüller,
Bruno Woltzenlogel Paleo
Abstract:
The UITP workshop series brings together researchers interested in designing, developing and evaluating user interfaces for automated reasoning tools, such as interactive proof assistants, automated theorem provers, model finders, tools for formal methods, and tools for visualising and manipulating logical formulas and proofs. The eleventh edition of UITP took place in Vienna, Austria, and was par…
▽ More
The UITP workshop series brings together researchers interested in designing, developing and evaluating user interfaces for automated reasoning tools, such as interactive proof assistants, automated theorem provers, model finders, tools for formal methods, and tools for visualising and manipulating logical formulas and proofs. The eleventh edition of UITP took place in Vienna, Austria, and was part of the Vienna Summer of Logic, the largest ever joint conference in the area of Logic. This proceedings contains the eight contributed papers that were accepted for presentation at the workshop as well as the two invited papers.
△ Less
Submitted 28 October, 2014;
originally announced October 2014.
-
Formalization, Mechanization and Automation of Gödel's Proof of God's Existence
Authors:
Christoph Benzmüller,
Bruno Woltzenlogel Paleo
Abstract:
Gödel's ontological proof has been analysed for the first-time with an unprecedent degree of detail and formality with the help of higher-order theorem provers. The following has been done (and in this order): A detailed natural deduction proof. A formalization of the axioms, definitions and theorems in the TPTP THF syntax. Automatic verification of the consistency of the axioms and definitions wi…
▽ More
Gödel's ontological proof has been analysed for the first-time with an unprecedent degree of detail and formality with the help of higher-order theorem provers. The following has been done (and in this order): A detailed natural deduction proof. A formalization of the axioms, definitions and theorems in the TPTP THF syntax. Automatic verification of the consistency of the axioms and definitions with Nitpick. Automatic demonstration of the theorems with the provers LEO-II and Satallax. A step-by-step formalization using the Coq proof assistant. A formalization using the Isabelle proof assistant, where the theorems (and some additional lemmata) have been automated with Sledgehammer and Metis.
△ Less
Submitted 3 September, 2017; v1 submitted 21 August, 2013;
originally announced August 2013.
