Please use this identifier to cite or link to this item:
https://research.matf.bg.ac.rs/handle/123456789/471
Title: | CDCL-based abstract state transition system for coherent logic | Authors: | Nikolić, Mladen Janičić, Predrag |
Affiliations: | Informatics and Computer Science Informatics and Computer Science |
Keywords: | abstract state transition systems;CDCL SAT solving;coherent logic;machine verifiable proofs;readable proofs | Issue Date: | 17-Aug-2012 | Related Publication(s): | International Conference on Intelligent Computer Mathematics CICM 2012 | Journal: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Abstract: | We present a new, CDCL-based approach for automated theorem proving in coherent logic - an expressive semi-decidable fragment of first-order logic that provides potential for obtaining human readable and machine verifiable proofs. The approach is described by means of an abstract state transition system, inspired by existing transition systems for SAT and represents its faithful lifting to coherent logic. The presented transition system includes techniques from which CDCL SAT solvers benefited the most (backjumping and lemma learning), but also allows generation of human readable proofs. In contrast to other approaches to theorem proving in coherent logic, reasoning involved need not to be ground. We prove key properties of the system, primarily that the system yields a semidecision procedure for coherent logic. As a consequence, the semidecidability of another fragment of first order logic which is a proper superset of coherent logic is also proven. © 2012 Springer-Verlag. |
URI: | https://research.matf.bg.ac.rs/handle/123456789/471 | ISBN: | 9783642313738 | ISSN: | 03029743 | DOI: | 10.1007/978-3-642-31374-5_18 |
Appears in Collections: | Research outputs |
Show full item record
SCOPUSTM
Citations
2
checked on Dec 18, 2024
Page view(s)
11
checked on Dec 24, 2024
Google ScholarTM
Check
Altmetric
Altmetric
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.