LARA

Automating Satisfiability Proofs for First-Order Logic

First-order logic can be used to aximatize essentially all of math, through set theory.

Goal: a procedure such that if $S$ is a first-order formula (or an enumerable sequence of formulas i.e. sequence where we can compute $k$-the element for each $k$), then we can detect in finite amount of time the case when $S$ is unsatisfiable

Observations:

  • to prove $F$ is valid, we show $\lnot F$ is unsatisfiable
  • to show that $F$ is true in an axiomatization given as an enumerable sequence $S$, we check that the sequence $\lnot F$; $S$ is unsatisfiable
  • given a well-defined mathematical statement, we can detect in finite amount of time if this statement follows from a well-defined set of axioms

Hilbert's program

First-Order Provers in Verification

Countable Models for Quantified First-Order Logic

Resolution in First-Order Logic

Herbrand Theorem for Formulas with Equality