On Model-Based Reasoning: Recent Trends and
          Current Developments

                            Maria Paola Bonacina

        Dipartimento di Informatica Università degli Studi di Verona



   Abstract. 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 rea-
   soner 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.