Horace Blanc is doing his MPRI M2 internship at Parsifal under the supervision of Beniamino Accattoli. He will be working on Lambda to Pi.
The following papers authored by members of the Parsifal team were accepted to the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015):
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.
Today is the first day for both Beniamino Accattoli (CR) and Tomer Libal (Engineer). Welcome onboard!
We have several new arrivals in Parsifal.
- Roberto Blanco (supervised by Dale Miller)
- Sonia Marin (supervised by Dale Miller and Lutz Straßburger)
- Tomer Libal (starting 1 Jan, 2015)
The following four papers authored by Parsifal team members have been accepted to CSL-LICS 2014:
- Anupam Das. Pigeonhole and related combinatorial principles in deep inference and monotone systems
- Danko Ilik. Axioms and Decidability for Type Isomorphism in Presence of Sums
- Nicolas Guenot and Lutz Strassburger. Symmetric Normalisation for Intuitionistic Logic
- Kaustuv Chaudhuri and Nicolas Guenot. Equality and Fixpoints in the Calculus of Structures
The next round of the Reading Group on Fixed Points (RGFP) will be on Thursday, March 27. We will discuss some results from descriptive complexity theory and their relation to structural proof theory. Of particular interest is the open question of defining a logic for PTIME.