ABSTRACT. The nominal approach to the specification of languages with binding operators, introduced by Gabbay and Pitts, has its roots in nominal set theory. With a user-friendly first-order syntax, nominal logic provides a formal framework to reason about binding operators similar to conventional, on-paper reasoning. Indeed, nominal logic uses the well-understood concept of permutation groups acting on sets to provide a rigorous first-order treatment for the common informal practice of fresh and bound names. 

In this talk, I will present our current work towards incorporating nominal techniques into two widely-used rule-based first-order verification environments: the K specification framework and the Maude programming environment.

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.

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.

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.