Invited talks



Maria Paola Bonacina (Dip. Informatica, Università di Verona)

On Model-Based Reasoning: Recent Trends and Current Developments

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.



Eugenio G. Omodeo (DMG sez. Matematica e Informatica, Università di Trieste)

Proof verification within set theory

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.



Alberto Policriti (Dip. Matematica e Informatica, Università di Udine)

On the decidability of the ∃*∀* prefix class in Set Theory

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.





Tutorial

Joanna Golińska-Pilarek (Inst. Philosophy, University of Warsaw)

Relational Dual Tableaux: Foundations and Applications

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.


References

[GHM13] J. Golińska-Pilarek, T. Huuskonen, E. Muñoz-Velasco, “Relational dual tableau decision procedures and their applications to modal and intuitionistic logics”, forthcoming in Annals of Pure and Applied Logics, doi: 10.1016/j.apal.2013.06.003
[ORG11] E. Orłowska, J. Golińska-Pilarek, Dual Tableaux: Foundations, Methodology, Case Studies, Springer, 2011.
[ORŁ88] E. Orłowska, “Relational interpretation of modal logics”, in: H. Andreka, D. Monk, I. Nemeti (eds.), Algebraic Logic, Colloquia Mathematica Societatis Janos Bolyai 54, North Holland, Amsterdam, 1988, 443-471.
[RAS60] H. Rasiowa, R. Sikorski, “On Gentzen theorem”, Fundamenta Mathematicae 48 (1960), 57-69.
[TAR41] A. Tarski, “On the calculus of relations”, Journal of Symbolic Logic 6 (1941), 73- 89.