Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/528
DC FieldValueLanguage
dc.contributor.authorJaničić, Predragen_US
dc.contributor.authorNarboux, Julienen_US
dc.date.accessioned2022-08-13T10:14:44Z-
dc.date.available2022-08-13T10:14:44Z-
dc.date.issued2022-
dc.identifier.issn01687433en
dc.identifier.urihttps://research.matf.bg.ac.rs/handle/123456789/528-
dc.description.abstractIn contrast to common automated theorem proving approaches, in which the search space is a set of some formulae and what is sought is again a (goal) formula, we propose an approach based on searching for a proof (of a given length) as a whole. Namely, a proof of a formula in a fixed logical setting can be encoded as a sequence of natural numbers meeting some conditions and a suitable constraint solver can find such a sequence. The sequence can then be decoded giving a proof in the original theory language. This approach leads to several unique features, for instance, it can provide shortest proofs. In this paper, we focus on proofs in coherent logic, an expressive fragment of first-order logic, and on SAT and SMT solvers for solving sets of constraints, but the approach could be tried in other contexts as well. We implemented the proposed method and we present its features, perspectives and performances. One of the features of the implemented prover is that it can generate human understandable proofs in natural language and also machine-verifiable proofs for the interactive prover Coq.en_US
dc.relation.ispartofJournal of Automated Reasoningen_US
dc.subjectAutomated theorem provingen_US
dc.subjectCoherent logicen_US
dc.subjectConstraint solvingen_US
dc.subjectInteractive theorem provingen_US
dc.subjectSAT/SMT solvingen_US
dc.titleTheorem Proving as Constraint Solving with Coherent Logicen_US
dc.typeArticleen_US
dc.identifier.doi10.1007/s10817-022-09629-z-
dc.identifier.scopus2-s2.0-85130210678-
dc.identifier.urlhttps://api.elsevier.com/content/abstract/scopus_id/85130210678-
dc.contributor.affiliationInformatics and Computer Scienceen_US
dc.relation.firstpage689en_US
dc.relation.lastpage746en_US
dc.relation.volume66en_US
dc.relation.issue4en_US
item.fulltextNo Fulltext-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.cerifentitytypePublications-
item.grantfulltextnone-
item.openairetypeArticle-
crisitem.author.deptInformatics and Computer Science-
crisitem.author.orcid0000-0001-8922-4948-
Appears in Collections:Research outputs
Show simple item record

SCOPUSTM   
Citations

2
checked on Dec 20, 2024

Page view(s)

24
checked on Dec 24, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.