Pérez, JAN;
Voronkov, A;
(2008)
Proof systems for effectively propositional logic.
In: Armando, A and Baumgartner, P and Dowek, G, (eds.)
Automated Reasoning. 4th International Joint Conference, IJCAR 2008 Sydney, Australia, August 12-15, 2008 Proceedings.
(pp. 426 - 440).
Springer Berlin Heidelberg
![[thumbnail of ijcar08.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
ijcar08.pdf Download (187kB) |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Proof systems for effectively propositional logic |
| Event: | IJCAR 2008 Sydney, Australia, August 12-15, 2008 |
| ISBN-13: | 978-3-540-71069-1 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-540-71070-7_36 |
| Publisher version: | http://dx.doi.org/10.1007/978-3-540-71070-7_36 |
| Language: | English |
| Additional information: | This is the authors' accepted manuscript of this published chapter. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1361366 |
Archive Staff Only
 |
View Item |
