Invariant-free clausal temporal resolution

DOI10.1007/S10817-011-9241-2zbMATH Open1408.03006OpenAlexW2010166872MaRDI QIDQ352974FDOQ352974

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

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

zbMATH Keywords

resolutionclausal normal forminvariant-freepropositional linear-time temporal logic

Mathematics Subject Classification ID

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

Cites Work

• Temporal logic. Vol. 2. Mathematical foundations and computational aspects
• Title not available (Why is that?)
• Title not available (Why is that?)
• Temporal logic can be more expressive
• A Machine-Oriented Logic Based on the Resolution Principle
• Tableau methods for modal and temporal logics
• Dual systems of tableaux and sequents for PLTL
• The complementation problem for Büchi automata with applications to temporal logic
• Temporalising tableaux
• Systematic semantic tableaux for PLTL
• An introduction to practical formal methods using temporal logic
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Logic for computer scientists

Cited In (3)

• Title not available (Why is that?)
• Title not available (Why is that?)
• \((\alpha, \beta)\)-ordered linear resolution of intuitionistic fuzzy propositional logic

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)