@inproceedings{0fbbbccf392f45e3a3bed36c2a809786,
title = "Proof systems for effectively propositional logic",
abstract = "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. {\textcopyright} 2008 Springer-Verlag Berlin Heidelberg.",
author = "Navarro, {Juan Antonio} and Andrei Voronkov",
year = "2008",
doi = "10.1007/978-3-540-71070-7_36",
language = "English",
isbn = "3540710698",
volume = "5195",
series = "Lecture Notes in Computer Science",
publisher = "Springer Nature",
pages = "426--440",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",
address = "United States",
note = "4th International Joint Conference on Automated Reasoning, IJCAR 2008 ; Conference date: 01-07-2008",
}