Relational dual tableaux for interval temporal logics ★

References

• ALLEN , J. F. 1983 . Maintaining Knowledge about Temporal Intervals . Communications of the ACM , 26 ( 11 ) : 832 – 843 .
   Web of Science ®Google Scholar
• BOWMAN , H. and THOMPSON , S. 2003 . A decision procedure and complete axiomatization of finite interval temporal logic with projection . Journal of Logic and Computation , 13 ( 2 ) : 195 – 239 .
   Web of Science ®Google Scholar
• BRESOLIN , D. and MONTANARI , A. 2005 . A tableau-based decision procedure for a branching-time interval temporal logic . Proceedings of M4M- 4: 4th International Workshop on Methods for Modalities . December 2005 , Berlin , Germany. Edited by: SCHLINGLOFF , H. pp. 38 – 53 .
   Google Scholar
• BRESOLIN , D. and MONTANARI , A. 2005 . A tableau-based decision procedure for Right Propositional Neighborhood Logic . Proceedings of TABLEAUX 2005, vol. 3702 of LNAI . September 2005 , Koblenz , Germany. pp. 63 – 77 . Springer .
   Google Scholar
• BRESOLIN , D. , MONTANARI , A. and SCIAVICCO , G. 2006 . An optimal decision procedure for Right Propositional Neighborhood Logic . Journal of Automated Reasoning , to appear
   Web of Science ®Google Scholar
• CHAOCHEN , Z. and HANSEN , M. R. 1998 . “ An Adequate First Order Interval Logic ” . In Compositionality: the Significant Difference, vol. 1536 of LNCS , Edited by: DE ROEVER , W. , LANGMARK , H. and PNUELI , A. 584 – 608 . Springer .
   Google Scholar
• DALLIEN , J. and MACCAULL , W. 2005 . RelDT: A relational dual tableaux automated theorem prover preprint
   Google Scholar
• DILLON , L. , KUTTY , G. , MOSER , L. , MELLIAR-SMITH , P. M. and RAMAKRISHNA , Y. An Automata-Theoretic Decision Procedure for Future Interval Logic . Proceedings of the 12th Software Technology and Theoretical Computer Science, vol. 652 of LNCS . Edited by: Ed , R. S. pp. 51 – 67 .
   Google Scholar
• DILLON , L. , KUTTY , G. , MOSER , L. , MELLIAR-SMITH , P. M. and RAMAKRISHNA , Y. A Real-Time Interval Logic and Its Decision Procedure . Proceedings of th 13th Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 761 of LNCS . pp. 173 – 192 . Springer .
   Google Scholar
• DILLON , L. , KUTTY , G. , MOSER , L. , MELLIAR-SMITH , P. M. and RAMAKRISHNA , Y. 1996 . Interval Logics and their Decision Procedures. Part II: a Real-Time Interval Logic . Theoretical Computer Science , 170 ( 1–2 ) : 1 – 47 .
   Web of Science ®Google Scholar
• DILLON , L. , KUTTY , G. , MOSER , L. , MELLIAR-SMITH , P. M. and RAMAKRISHNA , Y. 1996 . nterval Logics and their Decision Procedures. Part I: an interval logic . Theoretical Computer Science , 166 ( 1–2 ) : 1 – 47 .
   Web of Science ®Google Scholar
• FORMISANO , A. , ORŁOWSKA , E. and OMODEO , E. 2005 . “ A PROLOG tool for relational translation of modal logics: A front-end for relational proof systems ” . In TABLEAUX 2005 Position Papers and Tutorial Descriptions , Fachberichte Informatik No 12 Edited by: BECKERT , B. 1 – 10 . Universitaet Koblenz-Landau .
   Google Scholar
• GOLIŃSKA-PILAREK , J. and ORŁOWSKA , E. 2006 . Relational logics and their applications submitted
   Google Scholar
• GOLIŃSKA-PILAREK , J. and ORŁOWSKA , E. 2006 . Tableaux and Dual Tableaux: Transformation of proofs . Studia Logica , to appear
   Google Scholar
• GORANKO , V. , MONTANARI , A. and SCIAVICCO , G. A general tableau method for propositional interval temporal logic . Proceedings of the International Conference TABLEAUX 2003, vol. 2796 of LNAI . pp. 102 – 116 . Springer .
   Google Scholar
• GORANKO , V. , MONTANARI , A. and SCIAVICCO , G. 2003 . Propositional interval neighborhood temporal logics . Journal of Universal Computer Science , 9 ( 9 ) : 1137 – 1167 .
   Web of Science ®Google Scholar
• GORANKO , V. , MONTANARI , A. and SCIAVICCO , G. 2004 . A road map of interval temporal logics and duration calculi . Journal of Applied Non-Classical Logics , 14 ( 1–2 ) : 9 – 54 .
   Google Scholar
• GORANKO , V. , MONTANARI , A. , SCIAVICCO , G. and SALA , P. 2006 . A general tableau method for propositional interval temporal logics: theory and implementation . Journal of Applied Logic , to appear
   Google Scholar
• HALPERN , J. and SHOHAM , Y. 1991 . A propositional modal logic of time intervals . Journal of the ACM , 38 ( 4 ) : 935 – 962 .
   Web of Science ®Google Scholar
• LADKIN , P. B. and MADDUX , R. 1987 . The algebra of convex time intervals , Palo Alto , California : Kestrel Institute . report num. KES.U.87.2
   Google Scholar
• LODAYA , K. Sharpening the Undecidability of Interval Temporal Logic . Proc. of 6th Asian Computing Science Conference, vol. 1961 of LNCS . pp. 290 – 298 . Springer .
   Google Scholar
• MACCAULL , W. and ORŁOWSKA , E. 2002 . Correspondence results for relational proof systems with applications to the Lambek calculus . Studia Logica , 71 : 279 – 304 .
   Google Scholar
• MONTANARI , A. , SCIAVICCO , G. and VITACOLONNA , N. Decidability of interval temporal logics over split-frames via granularity . Proc. of the 8th European Conference on Logic in Artificial Intelligence, vol. 2424 of LNAI . pp. 259 – 270 . Springer .
   Google Scholar
• MOSZKOWSKI , B. 1983 . Reasoning about digital circuits , Stanford , CA : Dept. of Computer Science, Stanford University . Tech. Rep. STAN-CS-83-970
   Google Scholar
• ORŁOWSKA , E. 1988 . “ Relational interpretation of modal logics ” . In Algebraic Logic, vol. 54 of Colloquia Mathematica Societatis Janos Bolyai Edited by: ANDREKA , H. , MONK , D. and NEMETI , I. 443 – 471 . North Holland, Amsterdam
   Google Scholar
• ORŁOWSKA , E. 1995 . “ Temporal logics in a relational framework ” . In Time and Logic – a Computational Approach , Edited by: BOLC , L. and SZALAS , A. 249 – 277 . University College London Press .
   Google Scholar
• ORŁOWSKA , E. 1996 . “ Relational proof systems for modal logics ” . In Proof Theory of Modal Logics , Edited by: WANSING , H. 55 – 77 . Kluver .
   Google Scholar
• RASIOWA , H. and SIKORSKI , R. 1963 . The Mathematics of Metamathematics , Warsaw : Polish Scientific Publishers .
   Google Scholar
• RASMUSSEN , T. Labelled Natural Deduction for Interval Logics . Proceedings of the Annual European Conference on Computer Science Logic CSL'2001, vol. 2142 of LNCS . Edited by: Ed , L. F. pp. 308 – 323 . Springer .
   Google Scholar
• RASMUSSEN , T. 2001 . A Sequent Calculus for Signed Interval Logics , Informatics and Mathematical Modeling, Technical University of Denmark . report num. IMM-TR-2001-06
   Google Scholar
• VENEMA , Y. 1990 . Expressiveness and Completeness of an Interval Tense Logic . Notre Dame Journal of Formal Logic , 31 ( 4 ) : 529 – 547 .
   Google Scholar
• VENEMA , Y. 1991 . A modal logic for chopping intervals . Journal of Logic and Computation , 1 ( 4 ) : 453 – 476 .
   Google Scholar