×

LWB

swMATH ID: 1820
Software Authors: Goré, Rajeev; Heinle, Wolfgang; Heuerding, Alain
Description: Relations between propositional normal modal logics: An overview. In this short paper the authors give a useful overview of the most common propositional normal modal logics by first providing a catalogue of their axioms (and of the alternative names that have been considered in the standard textbooks, papers and reports), and then investigating the relationships between the logics; the equivalence between multiple axiomatizations of a logic is established by showing the interderivability of the different axioms. In doing so, the authors introduce the Logics Workbench LWB, a theorem prover for propositional modal and other nonclassical logics. A pleasant side effect of their work is the fact that their catalogue of axioms provides a database of theorems that can be used as a basic benchmark for testing and comparing the performance of different theorem provers for modal logics.
Homepage: https://academic.oup.com/logcom/article/7/5/649/970231
Keywords: propositional normal modal logics; axiomatizations; logics workbench LWB; theorem prover; database of theorems; survey
Related Software: MSPASS; TPTP; VAMPIRE; MiniSat
Cited in: 3 Publications

Citations by Year