Theorem Proving Using Clausal Resolution: From Past to Present

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


Modal and temporal logics are extensions to classical logic that have operators that deal with necessity and possibility (modal logics) and such as sometime, always and next (temporal logics). Models are sets of worlds that are connected by an accessibility relation. Restrictions imposed on this relation and the operators allowed give rise to different families of logic. This paper discusses an approach to theorem proving for temporal and modal logics based on clausal resolution. The main ideas are the translation to a normal form and the application of resolution rules that relate to the same world. This research initially focused on propositional linear time temporal logic but has been extended to computation tree logic, monodic first order temporal logic and normal modal logics. We describe the approach, explain the adaptations necessary for the logics mentioned and discuss the results of the provers developed for these logics.
Original languageEnglish
Title of host publicationInternational Conference on Reachability Problems
Subtitle of host publicationRP 2021: Reachability Problems
Publication statusPublished - 22 Oct 2021

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Link
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Theorem Proving Using Clausal Resolution: From Past to Present'. Together they form a unique fingerprint.

Cite this