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.
Mar 14
