An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic

DOI10.1007/978-3-540-70918-3_47zbMATH Open1141.03308OpenAlexW32421893MaRDI QIDQ3590963FDOQ3590963

Davide Bresolin, Pietro Sala, Angelo Montanari

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

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

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)

Cited In (14)

• 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
• Interval temporal logics over strongly discrete linear orders: expressiveness and complexity
• An optimal decision procedure for right propositional neighborhood logic
• Complete and Terminating Tableau for the Logic of Proper Subinterval Structures Over Dense Orderings
• Metric propositional neighborhood logic with an equivalence relation
• Optimal decision procedures for MPNL over finite structures, the natural numbers, and the integers
• Automated Reasoning with Analytic Tableaux and Related Methods
• Optimal Tableaux for Right Propositional Neighborhood Logic over Linear Orders
• Hybrid Metric Propositional Neighborhood Logics with Interval Length Binders
• Reactive synthesis from interval temporal logic specifications
• Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders
• A separation theorem for discrete-time interval temporal 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)