An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic

DOI10.1007/978-3-540-70918-3_47zbMath1141.03308MaRDI QIDQ3590963

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

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

03B70: Logic in computer science

03B25: Decidability of theories and sets of sentences

03B35: Mechanization of proofs and logical operations

03B44: Temporal logic

Related Items

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