Invariant-free clausal temporal resolution

DOI10.1007/S10817-011-9241-2MaRDI QIDQ352974zbMATH OpenOpenAlexFDO

Authors Jose Gaintzarain, M. Hermo, P. Lucio, Marisa Navarro, Fernando Orejas

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)

Recommendations

• A clausal resolution method for CTL branching-time temporal logic
• scientific article; zbMATH DE number 1980919
• scientific article; zbMATH DE number 1950255
• Clausal temporal resolution
• scientific article; zbMATH DE number 67448

Cites work

• scientific article; zbMATH DE number 3871318 (Why is no real title available?)
• scientific article; zbMATH DE number 3904560 (Why is no real title available?)
• scientific article; zbMATH DE number 3974944 (Why is no real title available?)
• scientific article; zbMATH DE number 747023 (Why is no real title available?)
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 48763 (Why is no real title available?)
• scientific article; zbMATH DE number 67448 (Why is no real title available?)
• scientific article; zbMATH DE number 1950255 (Why is no real title available?)
• A Cut-Free and Invariant-Free Sequent Calculus for PLTL
• A Machine-Oriented Logic Based on the Resolution Principle
• A clausal resolution method for CTL branching-time temporal logic
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• An empirical analysis of modal theorem provers
• An introduction to practical formal methods using temporal logic
• Dual systems of tableaux and sequents for PLTL
• Logic for computer scientists
• Nonclausal deduction in first-order temporal logic
• One-Pass Tableaux for Computation Tree Logic
• Propositional temporal logics: decidability and completeness
• Systematic semantic tableaux for PLTL
• Tableau methods for modal and temporal logics
• Tableau-Based Procedure for Deciding Satisfiability in the Full Coalitional Multiagent Epistemic Logic
• Temporal logic can be more expressive
• Temporal logic. Vol. 2. Mathematical foundations and computational aspects
• Temporalising tableaux
• The complementation problem for Büchi automata with applications to temporal logic

Cited in

(3)

• scientific article; zbMATH DE number 1444730 (Why is no real title available?)
• \((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic
• scientific article; zbMATH DE number 1980919 (Why is no real title available?)

Describes a project that uses

Uses Software

• TTM
• TRP++

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

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