An efficient relational deductive system for propositional non-classical logics

References

• BADBAN , B. and VAN DE POL , J. 2002 . Two Solutions to Incorporate Zero, Successor and Equality in Binary Decision Diagrams , The Netherlands : CWI Amsterdam . report
   Google Scholar
• BADBAN , B. and VAN DE POL , J. An Algorithm to Verify Formulas by Means of (0, s,=)-BDDs . Proceedings of CSICC04 .
   Google Scholar
• BADBAN , B. and VAN DE POL , J. 2005 . Zero, Successor and Equality in BDDs . Annals of Pure and Applied Logic , 133 ( 1-3 ) : 101 – 123 .
   Web of Science ®Google Scholar
• BECKERT , B. and GORÉ , R. Free Variable Tableaux for Propositional Modal Logics . Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, vol. 1227 ofLNCS . pp. 91 – 106 . Springer .
   Google Scholar
• BEHNKE , R. , BERGHAMMER , R. and SCHNEIDER , P. 1997 . Machine Support of Relational Computations: The Kiel RELVIEW System , Kiel , , Germany : Institut für Informatik und PraktischeMathematik, Christian-Albrechts-Universität . report num. Bericht Nr. 9711
   Google Scholar
• BERGHAMMER , R. , LEONIUK , B. and MILANESE , U. Implementation of Relational Algebra Using Binary Decision Diagrams . 6th International Conference on Relational Methods in Computer Science, RelMiCS 2001, vol. 2561 of LNCS . Edited by: DE SWART , H. pp. 241 – 257 .
   Google Scholar
• BOLLIG , B. and WEGENER , I. 1996 . Improving the Variable Ordering of OBDDs is NPcomplete . IEEE Transactions on Computers , 45 ( 9 ) : 993 – 1002 . IEEE Computer Society Press
   Web of Science ®Google Scholar
• BRINK , C. , KAHL , W. and SCHMIDT , G. 1997 . “ Relational Methods in Computer Science ” . In Advances in Computing Science , Springer .
   Google Scholar
• BROWN , C. and HUTTON , G. Categories, Allegories and Circuit Design . Proceedings, 9th Annual IEEE Symposium on Logic in Computer Science . pp. 372 – 381 . IEEE Computer Society Press .
   Google Scholar
• BROWN , C. and JEFFREY , A. Allegories of Circuits . The 3rd International Symposium on Logical Foundations of Computer Science . pp. 56 – 68 .
   Google Scholar
• BRYANT , R. E. 1986 . Graph-Based Algorithms for Boolean Function Manipulation . IEEE Transactions on Computers , C-35 ( 8 ) : 677 – 691 .
   Web of Science ®Google Scholar
• BRYANT , R. E. 1992 . Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams . Computing Surveys , 24 ( 3 ) : 293 – 318 .
   Web of Science ®Google Scholar
• CANTONE , D. , FORMISANO , A. , OMODEO , E. and ZARBA , C. 2003 . Compiling Dyadic First-Order Specifications into Map Algebra . Theoretical Computer Science , 293 ( 2 ) : 447 – 475 .
   Web of Science ®Google Scholar
• DEL CERRO , L. F. , FAUTHOUX , D. , GASQUET , O. , HERZIG , A. , LONGIN , D. and MASSACCI , F. Lotrec: the Generic Tableau Prover for Modal and Description Logics 453 – 458 . Goré et al. [GOR 01]
   Google Scholar
• CURTIS , S. and LOWE , G. 1996 . Proofs with Graphs . Science of Computer Programming , 26 ( 1-3 ) : 197 – 216 .
   Web of Science ®Google Scholar
• D'AGOSTINO , M. 1992 . Are Tableaux an Improvement on Truth Tables? . Journal of Logic, Language and Information , 1 : 235 – 252 .
   Google Scholar
• D'AGOSTINO , M. and MONDADORI , M. 1994 . The Taming of the Cut . Journal of Logic and Computation , 4 : 285 – 319 .
   Google Scholar
• D'AGOSTINO , M. 1999 . Tableau Methods for Classical Propositional Logic In [DAG 99b]
   Google Scholar
• D'AGOSTINO , M. , GABBAY , D. M. , HÄHNLE , R. and POSEGGA , J. , eds. 1999 . Handbook of Tableau Methods , Dordrecht : Kluwer Academic Publishers .
   Google Scholar
• DAWSON , J. E. and GORÉ , R. A Mechanised Proof System for Relation Algebra using Display Logic . Proceedings of the European Workshop on Logics in Artificial Intelligence (JELIA-98), vol. 1489 of LNCS . Edited by: DIX , J. , DEL CERRO , L. F. and FURBACH , U. pp. 264 – 278 . Springer .
   Google Scholar
• DEMRI , S. and ORŁOWSKA , E. 2002 . “ Incomplete Information: Structure, Inference, Complexity ” . In Monographs in Theoretical Computer Science , An EATCS Series Springer .
   Google Scholar
• DÜNTSCH , I. and ORŁAWSKA , E. 2000 . A Proof System for Contact Relation Algebras . Journal of Philosophical Logic , 29 ( 3 ) : 241 – 262 .
   Web of Science ®Google Scholar
• DÜNTSCH , I. and ORŁOWSKA , E. 2001 . “ Beyond Modalities: Sufficiency and Mixed Algebras ” . In Relational Methods for Computer Science Applications , Edited by: ORŁOWSKA , E. and SZALAS , A. 277 – 299 . Heidelberg : Physica-Verlag .
   Google Scholar
• DÜNTSCH , I. , ORŁOWSKA , E. , RADZIKOWSKA , A. M. and VAKARELOV , D. 2004 . Relational Representation Theorems for Some Lattice-Based Structures . Journal on Relational Methods in Computer Science , 1 : 132 – 160 .
   Google Scholar
• DWYER , B. 1995 . LIBRA: a Lazy Interpreter of Binary Relational Algebra , Australia : Department of Computer Science University of Adelaide . report num. 95-10
   Google Scholar
• FORMISANO , A. , OMODEO , E. G. and SIMEONI , M. 2001 . A Graphical Approach to Relational Reasoning . Electronic Notes in Theoretical Computer Science , 44 ( 3 ) Elsevier Science
   Google Scholar
• FORMISANO , A. , OMODEO , E. G. and TEMPERINI , M. Instructing Equational Set- Reasoning with Otter 152 – 167 . Goré et al. [GOR 01]
   Google Scholar
• FORMISANO , A. , OMODEO , E. G. and TEMPERINI , M. 2001 . “ Layered Map Reasoning: An Experimental Approach Put to Trial on Sets ” . In Declarative Programming , Edited by: DOVIER , A. , MEO , M. C. and OMICINI , A. vol. 48 , Elsevier Science .
   Google Scholar
• FORMISANO , A. , OMODEO , E. G. and ORŁOWSKA , 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 Edited by: BECKERT , B. 1 – 10 .
   Google Scholar
• FORMISANO , A. , OMODEO , E. G. and ORŁOWSKA , E. 2006 . “ An Environment for Specifying Properties of Dyadic Relations and Reasoning about Them. II: Relational Presentation of Non-Classical Logics ” . In Theory and Applications of Relational Structures as Knowledge Instruments II Edited by: DE SWART , H. , ORŁOWSKA , E. , SCHMIDT , G. and ROUBENS , M. To appear
   Google Scholar
• GIESE , M. Jul. 2002 . Proof Search without Backtracking for Free Variable Tableaux , Jul. , Fakultät für Informatik, Universität Karlsruhe . PhD thesis
   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. 1990 . Modal Definability in Enriched Languages . Notre Dame Journal of Formal Logic , 31 : 81 – 105 .
   Google Scholar
• GORÉ , R. 1996 . “ Cut-Free Display Calculi for Relation Algebras ” . In CSL, vol. 1258 of LNCS 198 – 210 . Selected Papers of the Annual Conference of the Association for Computer Science Logic
   Google Scholar
• GORÉ , R. , POSEGGA , J. , SLATER , A. and VOGT , H. System Description: cardTAP: The First Theorem Prover on a Smart Card . Proceedings of the 15th International Conference on Automated Deduction, vol. 1502 of LNCS . pp. 239 – 248 .
   Google Scholar
• GORÉ , R. 1999 . Tableau Methods for Modal and Temporal Logics In [DAG 99b]
   Google Scholar
• GORÉ , R. , LEITSCH , A. and NIPKOW , T. , eds. Automated Reasoning: First International Joint Conference, IJCAR 2001. Proceedings, vol. 2083 of LNCS . Springer .
   Google Scholar
• GOUBAULT , J. 1994 . Proving with BDDs and Control of Information . Proceedings of the 12th International Conference on Automated Deduction, vol. 814 of LNCS . 1994 , Nancy , France. Edited by: BUNDY , A. pp. 499 – 513 . Springer .
   Google Scholar
• GOUBAULT , J. and POSEGGA , J. BDDs and Automated Deduction . Proceedings 8th International Symposium on Methodologies for Intelligent Systems ISMIS, vol. 869 of LNCS . Edited by: RAŚ , Z. W. and ZEMANKOVA , M. pp. 541 – 550 . Springer .
   Google Scholar
• GOUBAULT , J. 1995 . A BDD-Based Simplification and Skolemization Procedure . Journal of the IGPL , 3 ( 6 ) : 827 – 855 .
   Google Scholar
• GOUBAULT-LARRECQ , J. 1996 . Implementing Tableaux by Decision Diagrams , Universität Karlsruhe, Institut für Logik, Komplexität und Deduktionssysteme . report
   Google Scholar
• GROOTE , J. F. and VAN DE POL , J. Equational Binary Decision Diagrams . Logic for Programming and Automated Reasoning: 7th International Conference, LPAR 2000, vol. 1955 of LNCS . Edited by: PARIGOT , M. and VORONKOV , A. pp. 161 – 178 . Springer .
   Google Scholar
• GROOTE , J. F. and TVERETINA , O. 2003 . Binary Decision Diagrams for First-Order Predicate Logic . Journal of Logic and Algebraic Programing , 57 ( 1-2 ) : 1 – 22 .
   Google Scholar
• HATTENSPERGER , C. , BERGHAMMER , R. and SCHMIDT , G. RALF - A Relation- Algebraic Formula Manipulation System and Proof . Proc. of AMAST93 . Edited by: NIVAT , M. , RATTRAY , C. , RUS , T. and SCOLLO , G. Springer-Verlag .
   Google Scholar
• HENNESSY , M. C. B. 1980 . A Proof System for the First-Order Relational Calculus . Journal of Computer and System Sciences , 20 ( 1 ) : 96 – 110 .
   Web of Science ®Google Scholar
• HUMBERSTONE , L. 1983 . Inaccessible Worlds . Notre Dame Journal of Formal Logic , 24 : 346 – 352 .
   Google Scholar
• JÄRVINEN , J. and ORŁOWSKA , E. Relational Correspondences for Lattices with Operators . Proceedings of the 8th International Conference on Relational Methods in Computer Science (RelMiCS 8) . Edited by: DÜNTSCH , I. and WINTER , M.
   Google Scholar
• JIFENG , H. and HOARE , C. A. R. 1986 . Weakest Prespecifications, part 1 . Fundamenta Informaticae , IX : 51 – 84 . Part II ibidem IX:217–252
   Google Scholar
• KORF , R. E. 1985 . Depth-First Iterative Deepening: an Optimal Admissible Tree Search . Artificial Intelligence , 27 ( 1 ) : 97 – 109 .
   Web of Science ®Google Scholar
• KWATINETZ , M. 1981 . Problems of Expressibility in Finite Languages , Berkeley : Univ. of California . Doctoral Diss
   Google Scholar
• LEE , G. , LITTLE , R. , MACCAULL , W. and SPENCER , B. 2002 . ReVAT - Relational Validator by Analytic Tableaux , Antigonish , , Canada : Department of Mathematics, Statistics and Computer Science, St. Francis Xavier University . report
   Google Scholar
• LETZ , R. 1999 . First-Order Tableau Methods In [DAG 99b]
   Google Scholar
• MACCAULL , W. and ORLOWSKA , E. 2003 . A Logic of Typed Relations and its Applications to Relational Databases , Antigonish , , Canada : Department of Mathematics, Statistics and Computer Science, St. Francis Xavier University . report
   Google Scholar
• MADDUX , R. D. 1983 . A Sequent Calculus for Relation Algebras . Annals of Pure and Applied Logic , 25 : 73 – 101 .
   Web of Science ®Google Scholar
• MADDUX , R. D. 1991 . The Origin of Relation Algebras in the Development and Axiomatization of the Calculus of Relations . Studia Logica , 50 ( 3/4 ) : 421 – 455 .
   Google Scholar
• VON OHEIMB , D. and GRITZNER , T. F. RALL: Machine-Supported Proofs for Relational Algebra . Proceedings of the 14th International Conference on Automated Deduction, vol. 1249 of LNCS . Edited by: MCCUNE , W. pp. 380 – 394 . Springer .
   Google Scholar
• OHLBACH , H. J. , NONNENGART , A. , DE RIJKE , M. and GABBAY , D. M. 2001 . “ Encoding Two-Valued Non-Classical Logics in Classical Logic ” . In Handbook of Automated Reasoning , Edited by: ROBINSON , A. and VORONKOV , A. Vol. II , 1403 – 1486 . Elsevier Science B.V. . chapter 21
   Google Scholar
• ORŁOWSKA , E. 1988 . Proof System for Weakest Prespecification . Information Processing Letters , 27 ( 6 ) : 309 – 313 .
   Web of Science ®Google Scholar
• ORŁOWSKA , E. 1991 . “ Relational Interpretation of Modal Logics ” . In Algebraic Logic, vol. 54 of Colloquia mathematica Societatis Janos Bolyai Edited by: ANDRÉKA , H. , NEMETI , I. and MONK , D. 443 – 471 . North-Holland Amsterdam
   Google Scholar
• ORŁOWSKA , E. 1992 . Relational Proof System for Relevant Logics . Journal of Symbolic Logic , 57 ( 4 ) : 1425 – 1440 .
   Web of Science ®Google Scholar
• ORŁOWSKA , E. 1994 . “ Relational Semantics for Non-Classical Logics: Formulas are Relations ” . In Philosophical Logic in Poland , Edited by: WOLENSKI , J. 167 – 186 . Kluwer .
   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 . Univ. College London Press .
   Google Scholar
• ORŁOWSKA , E. 1996 . “ Relational Proof Systems for Modal Logics ” . In Proof Theory of Modal Logic , Edited by: WANSING , H. Vol. 2 , 55 – 77 . Kluwer .
   Google Scholar
• ORŁOWSKA , E. 1997 . “ Relational Formalisation of Nonclassical Logics ” . In Relational Methods in Computer Science , Advances in Computing Science, chapter 6 Edited by: BRINK , C. , KAHL , W. and SCHMIDT , G. 90 – 105 . Wien : Springer . New York
   Google Scholar
• ORŁOWSKA , E. and VAKARELOV , D. Lattice-Based Modal Algebras and Modal Logics . Logic, Methodology and Philosophy of Science. Proceedings of the 12th International Congress . Edited by: VALDES-VILLANUEVA , P. H. L. and WESTERSTAHL , D. pp. 147 – 170 . KCL Puplications .
   Google Scholar
• VAN DE POL , J. and TVERETINA , O. A BDD-Representation for the Logic of Equality and Uninterpreted Functions . Proceedings of MFCS, vol. 3618 of LNCS . pp. 769 – 780 .
   Google Scholar
• POSEGGA , J. and LUDÄSCHER , B. 1992 . “ Towards First-Order Deduction Based on Shannon Graphs ” . In GWAI, vol. 671 of LNCS , Edited by: OHLBACH , H. J. 67 – 75 . Springer .
   Google Scholar
• POSEGGA , J. and SCHMITT , P. H. 1995 . Automated Deduction with Shannon Graphs . Journal of Logic and Computation , 5 ( 6 ) : 697 – 729 .
   Web of Science ®Google Scholar
• POSEGGA , J. and SCHMITT , P. H. 1999 . Implementing Semantic Tableaux In [DAG 99b]
   Google Scholar
• RASIOWA , H. and SIKORSKI , R. 1963 . The Mathematics of Metamathematics , Polish Scientific Publishers .
   Google Scholar
• SCHÖNFELD , W. 1982 . Upper Bounds for a Proof-Search in a Sequent Calculus for Relational Equations . Zeitschrift fuer Mathematische Logic und Grundlagen der Mathematik , 28 : 239 – 246 .
   Web of Science ®Google Scholar
• SCHNEIDER , K. , KUMAR , R. and KROPF , T. 1994 . Accelerating Tableaux Proofs Using Compact Representations . Formal Methods in System Design , 5 ( 1-2 ) : 145 – 176 .
   Web of Science ®Google Scholar
• SCHÜTZ , H. and GEISLER , T. 2000 . Efficient Model Generation through Compilation . Information and Computation , 162 ( 1-2 ) : 138 – 157 . Academic Press
   Web of Science ®Google Scholar
• SINZ , C. System Description: ARA - An Automatic Theorem Prover for Relation Algebras . Proceedings of the 17th International Conference on Automated Deduction, vol. 1831 of LNCS . Edited by: MCALLESTER , D. A. pp. 177 – 182 . Springer .
   Google Scholar
• SMULLYAN , R. M. 1995 . First-Order Logic , second corrected edition , New York : Dover Publications . First published 1968 by Springer
   Google Scholar
• TARSKI , A. and GIVANT , S. A Formalization of Set Theory without Variables, vol. 41 of Colloquium Publications . American Mathematical Society .
   Google Scholar
• WEGENER , I. 2004 . BDDs-Design, Analysis, Complexity, and Applications . Discrete Applied Mathematics , 138 ( 1-2 ) : 229 – 251 .
   Web of Science ®Google Scholar
• WUNDERWALD , J. E. Memoing Evaluation by Source-to-Source Transformation . Proceedings of 5th LOPSTR, vol. 1048 of LNCS . pp. 17 – 32 .
   Google Scholar
• Web repository of computational tools for non-Classical logics, AiML http://www.cs.man.ac.uk/~schmidt/tools
   Google Scholar
• Web reference for SICStus Prolog http://www.sics.se/sicstus
   Google Scholar
• ZANTEMA , H. and VAN DE POL , J. 2001 . A Rewriting Approach to Binary Decision Diagrams . Journal of Logic and Algebraic Programing , 49 ( 1-2 ) : 61 – 86 .
   Google Scholar