Cittā Universitaria, viale Andrea Doria 6, 95125 Catania

Proofs and models are the mainstay of automated reasoning. Traditionally, proofs have taken center stage, because in first-order logic theorem proving is semi-decidable, and model building is not. The growth of algorithmic reasoning and of its applications to software has changed the balance, because if satisfiability is decidable, symmetry is restored, and models are useful for applications and intuitive for users. While first-order provers search for a proof and may use an interpretation to guide the search, algorithmic reasoners search for a model, use deduction to drive the search, and the candidate model to guide the deduction. Thus, the symmetry is also in the reasoner's operations. However, decidability comes at the expense of expressivity. After some historical perspective on the evolution from proof to model oriented reasoning, we present a method, named DPLL(Gamma+T), which integrates algorithmic reasoner and first-order prover, in such a way that each does what it is best at, and the prover also makes use of the candidate model.

The proof-checker ÆtnaNova, aka Ref, processes proof scenarios to establish
whether or not they are formally correct. A scenario, typically written by
a working mathematician or computer scientist, consists of definitions, theorem statements and proofs of the theorems. There is a construct enabling one to package definitions and theorems into reusable proofware components.

The deductive system underlying Ref—mainly first-order, but with an
important second-order feature: the packaging construct just mentioned—is
a variant of the Zermelo-Fraenkel set theory, ZFC, with axioms of regularity
and global choice. This is apparent from the very syntax of the language,
borrowing from the set-theoretic tradition many constructs, e.g. abstraction
terms. Much ofRef's naturalness, comprehensiveness, and readability, stems
from this foundation; much of its effectiveness, from the fifteen or so built-in
mechanisms, tailored on ZFC, which constitute its inferential armory.

Rather peculiar aspects of Ref, in comparison to other proof-assistants
(Mizar to mention one), are that Ref relies only marginally on predicate
calculus and that types play no significant role, in it, as a foundation.

This talk illustrates the state-of-the-art of proof-verification technology
based on set theory, by reporting on `proof-pearl' scenarios currently under
development and by examining some small-scale, yet significant, examples
of use of Ref. The choice of examples will reflect today's tendency to bring
Ref's scenarios closer to algorithm-correctness verification, mainly referred
to graphs.

The infinity axiom rarely plays a role in applications to algorithms; nevertheless
the availability of all resources of ZFC is important in general:
for example, relatively unsophisticated argumentations enter into the proof
that the Davis-Putnam-Logemann-Loveland satisfiability test is correct, but
in order to prove the compactness of propositional logic or Stone's representation
theorem for Boolean algebras one can fruitfully resort to Zorn's
lemma.

In this talk I will describe the set-theoretic version of the Classical Decision Problem for First Order Logic. I will then illustrate the result on the decidability of the satisfiability problem class of purely universal formulae (∃*∀*-sentences) on the unquantified language whose relational symbols are membership and equality. The class we studied is, in the classical (first order) case, the so-called Bernays-Schoenfinkel-Ramsey (BSR) class.

The set-theoretic decision problem calls for the existence of an algorithm that, given a purely universal formula in membership and equality, establishes whether there exist sets that substituted for the free variables will satisfy the formula. The sets to be used are pure sets, namely sets whose only possible elements are themselves sets.
Much of the difficulties in solving the decision problem for the BSR class in Set Theory came from the ability to express infinity in it, a property not shared by the classical BSR class. The result makes use of a set-theoretic version of the argument Ramsey used to characterize the spectrum of the BSR class in the classical case. This characterization was the result that motivated Ramsey celebrated combinatorial theorem.

The origin of dual tableaux goes back to the paper [RAS60] of Rasiowa and Sikorski, where a cut-free deduction system for the classical first-order logic has been presented. Systems in the Rasiowa-Sikorski style are ‘top-down’ validity checkers and they are dual to the well known tableau systems. The common language of most of relational dual tableaux is the logic of binary relations which was introduced in [ORŁ88] as a logical counterpart to the class of representable relation algebras given by Tarski in [TAR41].

The relational methodology enables us to represent within a uniform formalism the three basic components of formal systems: syntax, semantics, and deduction apparatus. Hence, the relational approach can be seen as a general framework for representing, investigating, implementing, and comparing theories with incompatible languages and/or semantics.

Relational dual tableaux are powerful tools which perform not only verification of validity (i.e., verification of truth of the statements in all the models of a theory) but often they can also be used for proving entailment (i.e., verification that truth of a finite number of statements implies truth of some other statement), model checking (i.e., verification of truth of a statement in a particular fixed model), and finite satisfaction (i.e., verification that a statement is satisfied by some fixed objects of a finite model).

This presentation is an introductory overview on specific methodological principles of constructing relational dual tableaux and their applications to non-classical logics. In particular, we will present relational dual tableaux for standard non-classical logics (modal, intuitionistic, relevant, many-valued) and for various applied theories of computational logic (fuzzy-set-based reasoning, qualitative reasoning, reasoning about programs, among others). Furthermore, we will discuss decision procedures in dual tableaux style. By way of example, we will show how to modify the classical dual tableau systems to obtain decision procedures for some modal and intuitionistic logics.

[ORG11] E. Orłowska, J. Golińska-Pilarek,

[ORŁ88] E. Orłowska, “Relational interpretation of modal logics”, in: H. Andreka, D. Monk, I. Nemeti (eds.),

[RAS60] H. Rasiowa, R. Sikorski, “On Gentzen theorem”,

[TAR41] A. Tarski, “On the calculus of relations”,