Taus Brock-Nannestad (Parsifal, Inria)

Title: Forcing Saturation in the Inverse Method

Abstract:
The Inverse Method is a marvellous method of proof search in classical
and non-classical logics. Among its nice features is the fact that any
sequent produced during proof search is indeed a valid theorem.
Unfortunately this feature is a double-edged sword. To disprove a
sequent using the inverse method requires finding all consequences of
the given assumptions, and checking that the goal sequent is not
contained therein. Naturally, this requires that this set of
consequences is finite. For all but the most trivial first-order
theories, there will be an infinite set of distinct consequences of the
assumptions, and hence this desired saturation becomes impossible to
achieve.

In my talk, I will describe a way of forcing the inverse method to
saturate, by performing the proof search with an over-approximation of
the given assumptions. This is sound for the purposes of disproving
sequents, and can be iteratively refined if an attempt at a disproof
yields an unsound proof instead.

The method has been implemented by myself and Kaustuv Chaudhuri in the
form of the Mætning theorem prover.