A mechanisation of classical modal tense logics using Isabelle

DOI10.1007/BFB0095045MaRDI QIDQ4247208zbMATH OpenFDO

Authors Rajeev Goré, Jeremy E. Dawson

Publication date 12 January 2000

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

Full work available at URL https://doi.org/10.1007/BFB0095045

zbMATH Keywords

automated deductiondisplay logichybrid logicsinteractive theorem provermulti-modal logicsproof assistant Isabelletense logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logics of knowledge and belief (including belief change) (03B42) Temporal logic (03B44) Modal logic (including the logic of norms) (03B45) Logic in artificial intelligence (68T27)

Recommendations

• A labelled sequent system for tense logic \(\mathbf {K}_t\)
• The foundation of a generic theorem prover
• TABLEAUX: A general theorem prover for modal logics
• Automated proof support for interval logics
• A mechanised proof system for relation algebra using display logic

Cited in

(2)

• Automated proof support for interval logics
• A labelled sequent system for tense logic \(\mathbf {K}_t\)

Describes a project that uses

Uses Software

• Isabelle

This page was built for publication: A mechanisation of classical modal tense logics using Isabelle

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