Checking proof transformations with ASP
Giselle Reis - TUWien (Austria) giselle@logic.at
Vivek Nigam, Leonardo Lima - UFPB (Brazil)
What is "this"? Proof transformation.
Finding the possible derivations
Combinatorial problem
ASP modeling
Abstract the contexts:
Apply cut and and-left:
Where does go?
Generate the facts:
For every possible proof in which rules r1 and r2 are applied, in this order, to a sequent S, there is a proof where r2 and r1 are applied, in this order, to S.
Each possibility generates a different derivation:
Using the rules:
Problem 1: Find the possible derivations using r1 then r2.
Problem 2: Decide if provability of a derivation implies the provability of another derivation.
Two models are generated, each describing one derivation!
Sequent calculus
Systems
Deciding provability implication
Putting things together
of sequents
Checking whether a rule r1 permutes over a rule r2
of derivations:
provable(d1) ---> provable(d2)
We specify the cases in which provability fails:
r1 first, then r2
D1
find derivations
reduces to sequents:
for all open leaves l2 in d2, there exists a leaf l1 in d1 such that
provable(l1) ---> provable(l2)
or
Input: rules r1 and r2, sequent format (contexts and their properties)
find derivations
(linear logic specifications)
(if F cannot be erased)
or
D2
r2 first, then r1
Check if for every d in D1, there is a d' in D2 such that
provable(d) ---> provable(d')
If yes, then the rules permute.
Sets of formulas
If no, then they might permute using more involved transformations.
Sound, but not complete.
Sequent:
Possibly divided in contexts
Inference rules:
case 1, case 2, ..., case 20, ...
Will this ever end?!?!
10 rules -> 90 permutations possible
https://code.google.com/p/sellf/
Thank you!!