An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic

DOI10.1007/978-3-540-70918-3_47zbMath1141.03308OpenAlexW32421893MaRDI 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

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

Related Items (11)

Metric propositional neighborhood logic with an equivalence relation ⋮ A separation theorem for discrete-time interval temporal logic ⋮ Optimal decision procedures for MPNL over finite structures, the natural numbers, and the integers ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions ⋮ Optimal Tableaux for Right Propositional Neighborhood Logic over Linear Orders ⋮ Interval temporal logics over strongly discrete linear orders: expressiveness and complexity ⋮ Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders ⋮ Hybrid Metric Propositional Neighborhood Logics with Interval Length Binders ⋮ Reactive synthesis from interval temporal logic specifications ⋮ Complete and Terminating Tableau for the Logic of Proper Subinterval Structures Over Dense Orderings

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