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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Andrei Voronkov, Juan Antonio Navarro Pérez
• Keywords: Automated Reasoning, CADE 2008, Ground Instantiation, Proof Systems, Propositional Logic