An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic

DOI10.1007/978-3-540-70918-3_47MaRDI QIDQ3590963zbMATH OpenOpenAlexFDO

Authors Davide Bresolin, Angelo Montanari, Pietro Sala

Publication date 3 September 2007

Published in STACS 2007 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70918-3_47

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44) Logic in computer science (03B70)

Recommendations

• Optimal tableau systems for propositional neighborhood logic over all, dense, and discrete linear orders
• An optimal decision procedure for right propositional neighborhood logic
• Automated Reasoning with Analytic Tableaux and Related Methods
• A tableau system for right propositional neighborhood logic over finite linear orders: an implementation
• On Decidability and Expressiveness of Propositional Interval Neighborhood Logics

Cited in

(17)

• The addition of temporal neighborhood makes the logic of prefixes and sub-intervals \textsc{ExpSpace-complete}
• A survey on temporal logics for specifying and verifying real-time systems
• Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions
• Hybrid metric propositional neighborhood logics with interval length binders
• A tableau system for right propositional neighborhood logic over finite linear orders: an implementation
• Interval temporal logics over strongly discrete linear orders: expressiveness and complexity
• An optimal decision procedure for right propositional neighborhood logic
• Metric propositional neighborhood logic with an equivalence relation
• Optimal decision procedures for MPNL over finite structures, the natural numbers, and the integers
• An optimal decision procedure for MPNL over the integers
• Optimal tableau systems for propositional neighborhood logic over all, dense, and discrete linear orders
• Automated Reasoning with Analytic Tableaux and Related Methods
• Optimal Tableaux for Right Propositional Neighborhood Logic over Linear Orders
• Reactive synthesis from interval temporal logic specifications
• Complete and terminating tableau for the logic of proper subinterval structures over dense orderings
• A separation theorem for discrete-time interval temporal logic
• A tableau system for instantial neighborhood logic

This page was built for publication: An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic

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