Introducing 

Prezi AI.

Your new presentation assistant.

Refine, enhance, and tailor your content, source relevant images, and edit visuals quicker than ever before.

Loading content…
Transcript

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!!

Maybe we can automate this!

are context variables

are formula variables

Cut-elimination?

Complete proof-search?

Learn more about creating dynamic, engaging presentations with Prezi