Implementing a fair monodic temporal logic prover

DOI10.3233/AIC-2010-0457MaRDI QIDQ3568221zbMATH OpenOpenAlexFDO

Authors M. Ludwig, Ullrich Hustadt

Publication date 17 June 2010

Published in AI Communications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/aic-2010-0457

zbMATH Keywords

monodic first-order temporal logicresolutiontheorem proving

Mathematics Subject Classification ID

Temporal logic (03B44) Learning and adaptive systems in artificial intelligence (68T05) Logic in artificial intelligence (68T27)

Recommendations

• Fair Derivations in Monodic Temporal Reasoning
• Temporal logic and fair discrete systems
• Implementing Temporal Logics: Tools for Execution and Proof
• Branching-time logics and fairness, revisited
• Improved Bounded Model Checking for a Fair Branching-Time Temporal Epistemic Logic
• Automated Reasoning
• Equality and monodic first-order temporal logic
• scientific article; zbMATH DE number 7280017
• Safety, liveness and fairness in temporal logic
• Executable temporal logic for non-monotonic reasoning

Cited in

(11)

• Parameterized verification of leader/follower systems via first-order temporal logic
• Theorem proving for pointwise metric temporal logic over the naturals via translations
• Extracting unsatisfiable cores for LTL via temporal resolution
• Theorem proving using clausal resolution: from past to present
• A Cookbook for Temporal Conceptual Data Modelling with Description Logics
• Deductive verification of simple foraging robotic behaviours
• First-order resolution methods for modal logics
• A new rule for LTL tableaux
• Fair Derivations in Monodic Temporal Reasoning
• Temporal reasoning over linear discrete time
• Automated Reasoning

Describes a project that uses

Uses Software

• E Theorem Prover
• VAMPIRE
• TSPASS

This page was built for publication: Implementing a fair monodic temporal logic prover

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