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. This lecture covers both classical and recent topics in model-based reasoning, where models take center stage as much as proofs.
Many approaches in AI revolve around proofs and models. A proof is a formal argument that a claim holds. A model is a formal description of a state of a system. Proofs and models are related: proving by refutation means showing that the negation of the claim has no model, so that the claim is valid; if the proofs fails, a model of the negation of the claim is a counter-example. Solving a set of constraints means finding a satisfying assignment for the variables, and such an assignment is a model; if the search for a model fails, there is a proof. From a proving perspective, a proof means success and its failure gives a model; from a solving perspective, a model means success and its absence gives a proof.
The choice of perspective depends on decidability, which is inversely related to expressivity. In first-order logic, theorem proving is semi-decidable, and model finding is not; the proving perspective prevails, and reasoners are provers. In propositional logic, and decidable first-order theories, decidability restores the symmetry; the solving perspective prevails, and reasoners are solvers.
Motivation and Aim
While the distinction between semi-decidable and decidable, or, equivalently, between infinite and finite search space, separates proving and solving, applications unite them. It is disappointing to have a theorem prover that finds proofs in first-order logic, but cannot solve problems in arithmetic, or having an SMT-solver that solves problems in arithmetic or bitvectors, but cannot handle quantifiers, that are ubiquitous, for instance, in program verification. Thus, the goal is to advance the integration of proving and solving.
A double challenge
Prover and solver operate differently. In first-order theorem proving model representation is difficult; there are models with infinite domain; models are not unique; problems are stated axiomatically as a set of clauses; there is no intended model; the reasoner performs inferences to get a contradiction; models or their non-existence remain implicit. In SAT and SMT solving a model is represented finitely by an assignment of values to variables; an interpretation is intended; the theory is defined by a set of models, rather than by a set of axioms; the reasoner searches for a model, by maintaining a candidate partial model and trying to complete it. How can we integrate first-order theorem prover and SMT-solver? How can we integrate inference and search so that they guide each other?
Maria Paola Bonacina