We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: A theorem prover and countermodel constructor for provability logic in HOL Light

Abstract: We introduce our implementation in HOL Light of a prototype of a general theorem prover for normal modal logics. In the present work, we start by considering G\"odel-L\"ob provability logic (GL). The methodology consists of a shallow embedding of a labelled sequent calculus for GL whose validity relies on our formalised proof in HOL Light of modal completeness for GL w.r.t. possible world semantics, that we present in the first part of the present work. Our theorem prover for GL is thus implemented as a tactic of HOL Light that formalises the proof search in the corresponding labelled sequent calculus, and works as a decision algorithm for that logic: if the algorithm positively terminates, the tactic succeeds in producing a HOL Light theorem stating that the input formula is a theorem of GL; if the algorithm negatively terminates, the tactic extracts a model falsifying the input formula. We discuss our code for the formal proof of modal completeness, and the design of our proof search algorithm. Furthermore some examples of both interactive and automated use of the latter are shown.
Comments: arXiv admin note: substantial text overlap with arXiv:2102.05945
Subjects: Logic in Computer Science (cs.LO); Logic (math.LO)
ACM classes: F.4.1; I.2.3
Cite as: arXiv:2205.03659 [cs.LO]
  (or arXiv:2205.03659v1 [cs.LO] for this version)

Submission history

From: Cosimo Perini Brogi [view email]
[v1] Sat, 7 May 2022 14:18:57 GMT (590kb,D)

Link back to: arXiv, form interface, contact.