View: session overviewtalk overview

10:30 | PRESENTER: Ahmed Bhayat ABSTRACT. Classically, in saturation based proof systems, unification has been considered as a sub-procedure that can be used to restrict inferences. However, it is also possible to move unification to the calculus level, making the unification rules inferences themselves. For calculi that rely on unification procedures that return large or even infinite sets of unifiers, integrating unification into the calculus may be an attractive method of dovetailing between carrying out unification and carrying out inferences. This applies, for example, to AC-superposition and higher-order superposition. In this paper, we show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation. |

11:00 | PRESENTER: Petra Hozzová ABSTRACT. We present an automated reasoning framework for synthesizing recursion-free programs using saturation-based theorem proving. Given a functional specification encoded as a first-order logical formula, we use a first-order theorem prover to both establish validity of this formula and discover program fragments satisfying the specification. As a result, when deriving a proof of program correctness, we also synthesize a program that is correct with respect to the given specification. We describe properties of the calculus that a saturation-based prover capable of synthesis should employ, and extend the superposition calculus in a corresponding way. We implemented our work in the first-order prover \vampire{}, extending the successful applicability of first-order proving to program synthesis. |

11:30 | SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning PRESENTER: Martin Bromberger ABSTRACT. We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition based reasoning is performed with respect to a fixed reduction ordering. The completeness proof relies on the grounding of the clause set. It builds a ground partial model according to the fixed ordering, where minimal false ground instances of clauses then trigger non-redundant superposition inferences. We define a respective strategy for the SCL calculus such that clauses learned by SCL and superposition inferences eventually coincide. From this perspective the SCL calculus can be viewed as a generalization of the superposition calculus. |