Sciweavers

CADE
2008
Springer

Proof Systems for Effectively Propositional Logic

14 years 3 months ago
Proof Systems for Effectively Propositional Logic
We consider proof systems for effectively propositional logic. First, we show that propositional resolution for effectively propositional logic may have exponentially longer refutations than resolution for this logic. This shows that methods based on ground instantiation may be weaker than non-ground methods. Second, we introduce a generalisation rule for effectively propositional logic and show that resolution for this logic may have exponentially longer proofs than resolution with generalisation. We also discuss some related questions, such as sort assignments for generalisation.
Andrei Voronkov, Juan Antonio Navarro Pérez
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Andrei Voronkov, Juan Antonio Navarro Pérez
Comments (0)