Implementing a fair monodic temporal logic prover

DOI10.3233/AIC-2010-0457zbMath1206.68283OpenAlexW1698862083MaRDI QIDQ3568221

Ullrich Hustadt, Michel Ludwig

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

theorem provingresolutionmonodic first-order temporal logic

Mathematics Subject Classification ID

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

Related Items (9)

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Parameterized verification of leader/follower systems via first-order temporal logic ⋮ A Cookbook for Temporal Conceptual Data Modelling with Description Logics ⋮ Theorem proving using clausal resolution: from past to present ⋮ Unnamed Item ⋮ Theorem proving for pointwise metric temporal logic over the naturals via translations ⋮ First-Order Resolution Methods for Modal Logics ⋮ Fair Derivations in Monodic Temporal Reasoning ⋮ Deductive verification of simple foraging robotic behaviours

Uses Software

• VAMPIRE
• TSPASS
• E Theorem Prover

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