A general theorem prover for quantified modal logics

DOI10.1007/3-540-45616-3_19MaRDI QIDQ4412865zbMATH OpenFDO

Authors Virginie Thion, Serenella Cerrito, Marta Cialdea Mayer

Publication date 17 July 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2381/23810266.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45)

Recommendations

• TABLEAUX: A general theorem prover for modal logics
• First-order modal tableaux
• Labelled modal logics: Quantifiers
• Free-variable tableaux for constant-domain quantified modal logics with rigid and non-rigid designation
• The MODPROF theorem prover

Cited in

(6)

• GQML
• Free-variable tableaux for constant-domain quantified modal logics with rigid and non-rigid designation
• Solving modal logic problems by translation to higher-order logic
• Solving quantified modal logic problems by translation to classical logics
• Anselm's God in Isabelle/HOL
• A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux

Describes a project that uses

Uses Software

• ModLeanTAP

This page was built for publication: A general theorem prover for quantified modal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4412865)