Invariant-free clausal temporal resolution

DOI10.1007/S10817-011-9241-2zbMath1408.03006OpenAlexW2010166872MaRDI QIDQ352974

Fernando Orejas, Montserrat Hermo, Jose Gaintzarain, Marisa Navarro, Paqui Lucio

Publication date: 5 July 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-011-9241-2

zbMATH Keywords

resolutionclausal normal forminvariant-freepropositional linear-time temporal logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Related Items (1)

\((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic

Uses Software

• TTM
• TRP++

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Dual systems of tableaux and sequents for PLTL
• The complementation problem for Büchi automata with applications to temporal logic
• Temporalising tableaux
• An Introduction to Practical Formal Methods Using Temporal Logic
• Temporal logic can be more expressive
• Nonclausal deduction in first-order temporal logic
• One-Pass Tableaux for Computation Tree Logic
• Tableau-Based Procedure for Deciding Satisfiability in the Full Coalitional Multiagent Epistemic Logic
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• A clausal resolution method for CTL branching-time temporal logic
• An empirical analysis of modal theorem provers
• Propositional temporal logics: decidability and completeness
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• A Machine-Oriented Logic Based on the Resolution Principle
• Logic for computer scientists

This page was built for publication: Invariant-free clausal temporal resolution