An optimal decision procedure for right propositional neighborhood logic

DOI10.1007/S10817-006-9051-0MaRDI QIDQ877892zbMATH OpenOpenAlexFDO

Authors Davide Bresolin, Angelo Montanari, Guido Sciavicco

Publication date 4 May 2007

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

Full work available at URL https://doi.org/10.1007/s10817-006-9051-0

zbMATH Keywords

interval temporal logicright propositional neighborhood logictableaux-based decision procedures

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Recommendations

• Automated Reasoning with Analytic Tableaux and Related Methods
• An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic
• Optimal tableau systems for propositional neighborhood logic over all, dense, and discrete linear orders
• Optimal Tableaux for Right Propositional Neighborhood Logic over Linear Orders
• On Decidability and Expressiveness of Propositional Interval Neighborhood Logics

Cites work

• scientific article; zbMATH DE number 1696444 (Why is no real title available?)
• scientific article; zbMATH DE number 3937153 (Why is no real title available?)
• scientific article; zbMATH DE number 1931665 (Why is no real title available?)
• A Decision Procedure and Complete Axiomatization of Finite Interval Temporal Logic with Projection
• A Modal Logic for Chopping Intervals
• A Road Map of Interval Temporal Logics and Duration Calculi
• A general tableau method for propositional interval temporal logics
• A general tableau method for propositional interval temporal logics: theory and implementation
• A propositional modal logic of time intervals
• Automated Reasoning with Analytic Tableaux and Related Methods
• Deciding full branching time logic
• Decision procedures and expressiveness in the temporal logic of branching time
• Two variable first-order logic over ordered domains

Cited in

(18)

• Optimal Tableaux for Right Propositional Neighborhood Logic over Linear Orders
• Automated Reasoning with Analytic Tableaux and Related Methods
• A new modal logic for reasoning about space: spatial propositional neighborhood logic
• A survey on temporal logics for specifying and verifying real-time systems
• Optimal tableau systems for propositional neighborhood logic over all, dense, and discrete linear orders
• Finite satisfiability of propositional interval logic formulas with multi-objective evolutionary algorithms
• Adding one or more equivalence relations to the interval temporal logic \(\mathsf{AB}\overline{\mathsf{B}}\)
• Optimal decision procedures for MPNL over finite structures, the natural numbers, and the integers
• An optimal decision procedure for MPNL over the integers
• An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic
• Interval temporal logics over strongly discrete linear orders: expressiveness and complexity
• On Decidability and Expressiveness of Propositional Interval Neighborhood Logics
• Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions
• The dark side of interval temporal logic: marking the undecidability border
• Metric propositional neighborhood logic with an equivalence relation
• A separation theorem for discrete-time interval temporal logic
• A tableau system for right propositional neighborhood logic over finite linear orders: an implementation
• Complete and terminating tableau for the logic of proper subinterval structures over dense orderings

This page was built for publication: An optimal decision procedure for right propositional neighborhood logic

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