An efficient relational deductive system for propositional non-classical logics. (English) Zbl 1186.03044
Summary: We describe a relational framework that uniformly supports formalization and automated reasoning in varied propositional modal logics. The proof system we propose is a relational variant of the classical Rasiowa-Sikorski proof system. We introduce a compact graph-based representation of formulae and proofs supporting an efficient implementation of the basic inference engine, as well as of a number of refinements. Completeness and soundness results are shown and a Prolog implementation is described.
MSC:
| 03B45 | Modal logic (including the logic of norms) |
| 03B35 | Mechanization of proofs and logical operations |
| 03B70 | Logic in computer science |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
References:
| [1] | BADBAN B., Two Solutions to Incorporate Zero, Successor and Equality in Binary Decision Diagrams (2002) |
| [2] | BADBAN B., Proceedings of CSICC04 |
| [3] | BADBAN B., Annals of Pure and Applied Logic 133 (1) pp 101– (2005) · Zbl 1064.03009 · doi:10.1016/j.apal.2004.10.005 |
| [4] | BECKERT B., Proceedings, International Conference on Theorem Proving with Analytic Tableaux and Related Methods, vol. 1227 ofLNCS pp 91– · Zbl 1089.68001 |
| [5] | BEHNKE R., Machine Support of Relational Computations: The Kiel RELVIEW System (1997) |
| [6] | BERGHAMMER R., 6th International Conference on Relational Methods in Computer Science, RelMiCS 2001, vol. 2561 of LNCS pp 241– |
| [7] | BOLLIG B., IEEE Transactions on Computers 45 (9) pp 993– (1996) · Zbl 1048.68571 · doi:10.1109/12.537122 |
| [8] | BRINK C., Advances in Computing Science (1997) |
| [9] | BROWN C., Proceedings, 9th Annual IEEE Symposium on Logic in Computer Science pp 372– |
| [10] | BROWN C., The 3rd International Symposium on Logical Foundations of Computer Science pp 56– |
| [11] | DOI: 10.1109/TC.1986.1676819 · Zbl 0593.94022 · doi:10.1109/TC.1986.1676819 |
| [12] | DOI: 10.1145/136035.136043 · doi:10.1145/136035.136043 |
| [13] | CANTONE D., Theoretical Computer Science 293 (2) pp 447– (2003) · Zbl 1025.68053 · doi:10.1016/S0304-3975(01)00355-3 |
| [14] | 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] · Zbl 0988.68592 |
| [15] | CURTIS S., Science of Computer Programming 26 (1) pp 197– (1996) · Zbl 0852.68070 · doi:10.1016/0167-6423(95)00025-9 |
| [16] | D’AGOSTINO M., Journal of Logic, Language and Information 1 pp 235– (1992) · Zbl 0793.03059 · doi:10.1007/BF00156916 |
| [17] | DOI: 10.1093/logcom/4.3.285 · Zbl 0806.03037 · doi:10.1093/logcom/4.3.285 |
| [18] | D’AGOSTINO M., Tableau Methods for Classical Propositional Logic (1999) · doi:10.1007/978-94-017-1754-0_2 |
| [19] | DOI: 10.1007/978-94-017-1754-0 · doi:10.1007/978-94-017-1754-0 |
| [20] | DAWSON J. E., Proceedings of the European Workshop on Logics in Artificial Intelligence (JELIA-98), vol. 1489 of LNCS pp 264– |
| [21] | DEMRI S., An EATCS Series, in: Monographs in Theoretical Computer Science (2002) |
| [22] | DÜNTSCH I., Journal of Philosophical Logic 29 (3) pp 241– (2000) · Zbl 0956.03052 · doi:10.1023/A:1004764610651 |
| [23] | DÜNTSCH I., Relational Methods for Computer Science Applications pp 277– (2001) |
| [24] | DÜNTSCH I., Journal on Relational Methods in Computer Science 1 pp 132– (2004) |
| [25] | DWYER B., LIBRA: a Lazy Interpreter of Binary Relational Algebra (1995) |
| [26] | FORMISANO A., Electronic Notes in Theoretical Computer Science 44 (3) (2001) |
| [27] | FORMISANO , A. OMODEO , E. G. and TEMPERINI , M. Instructing Equational Set- Reasoning with Otter 152–167. Goré et al. [GOR 01] · Zbl 0988.68164 |
| [28] | FORMISANO A., Declarative Programming 48 (2001) |
| [29] | FORMISANO A., TABLEAUX 2005 Position Papers and Tutorial Descriptions pp 1– (2005) |
| [30] | FORMISANO A., Theory and Applications of Relational Structures as Knowledge Instruments II (2006) |
| [31] | GIESE M., Proof Search without Backtracking for Free Variable Tableaux (2002) |
| [32] | GOLIŃSKA-PILAREK J., Studia Logica (2006) |
| [33] | DOI: 10.1305/ndjfl/1093635335 · Zbl 0706.03016 · doi:10.1305/ndjfl/1093635335 |
| [34] | GORÉ R., CSL, vol. 1258 of LNCS pp 198– (1996) |
| [35] | GORÉ R., Proceedings of the 15th International Conference on Automated Deduction, vol. 1502 of LNCS pp 239– |
| [36] | GORÉ R., Tableau Methods for Modal and Temporal Logics (1999) · Zbl 0972.03529 · doi:10.1007/978-94-017-1754-0_6 |
| [37] | GORÉ R., Automated Reasoning: First International Joint Conference, IJCAR 2001. Proceedings, vol. 2083 of LNCS · Zbl 0968.00052 · doi:10.1007/3-540-45744-5 |
| [38] | GOUBAULT J., Proceedings of the 12th International Conference on Automated Deduction, vol. 814 of LNCS pp 499– (1994) |
| [39] | GOUBAULT J., Proceedings 8th International Symposium on Methodologies for Intelligent Systems ISMIS, vol. 869 of LNCS pp 541– |
| [40] | GOUBAULT J., Journal of the IGPL 3 (6) pp 827– (1995) · doi:10.1093/jigpal/3.6.827 |
| [41] | GOUBAULT-LARRECQ J., Implementing Tableaux by Decision Diagrams (1996) |
| [42] | GROOTE J. F., Logic for Programming and Automated Reasoning: 7th International Conference, LPAR 2000, vol. 1955 of LNCS pp 161– |
| [43] | GROOTE J. F., Journal of Logic and Algebraic Programing 57 (1) pp 1– (2003) |
| [44] | HATTENSPERGER C., Proc. of AMAST93 |
| [45] | HENNESSY M. C. B., Journal of Computer and System Sciences 20 (1) pp 96– (1980) · Zbl 0431.68084 · doi:10.1016/0022-0000(80)90007-0 |
| [46] | DOI: 10.1305/ndjfl/1093870378 · Zbl 0487.03007 · doi:10.1305/ndjfl/1093870378 |
| [47] | JÄRVINEN J., Proceedings of the 8th International Conference on Relational Methods in Computer Science (RelMiCS 8) |
| [48] | JIFENG H., Fundamenta Informaticae pp 51– (1986) |
| [49] | KORF R. E., Artificial Intelligence 27 (1) pp 97– (1985) · Zbl 0573.68030 · doi:10.1016/0004-3702(85)90084-0 |
| [50] | KWATINETZ M., Problems of Expressibility in Finite Languages (1981) |
| [51] | LEE G., ReVAT - Relational Validator by Analytic Tableaux (2002) |
| [52] | LETZ R., First-Order Tableau Methods (1999) · Zbl 0972.03524 · doi:10.1007/978-94-017-1754-0_3 |
| [53] | MACCAULL W., A Logic of Typed Relations and its Applications to Relational Databases (2003) |
| [54] | MADDUX R. D., Annals of Pure and Applied Logic 25 pp 73– (1983) · Zbl 0528.03016 · doi:10.1016/0168-0072(83)90055-6 |
| [55] | MADDUX R. D., Studia Logica 50 (3) pp 421– (1991) · Zbl 0754.03042 · doi:10.1007/BF00370681 |
| [56] | VON OHEIMB D., Proceedings of the 14th International Conference on Automated Deduction, vol. 1249 of LNCS pp 380– |
| [57] | OHLBACH H. J., Handbook of Automated Reasoning pp 1403– (2001) · doi:10.1016/B978-044450813-3/50023-0 |
| [58] | ORŁOWSKA E., Information Processing Letters 27 (6) pp 309– (1988) · Zbl 0647.68108 · doi:10.1016/0020-0190(88)90218-9 |
| [59] | ORŁOWSKA E., Algebraic Logic, vol. 54 of Colloquia mathematica Societatis Janos Bolyai pp 443– (1991) |
| [60] | ORŁOWSKA E., Journal of Symbolic Logic 57 (4) pp 1425– (1992) · Zbl 0794.03031 · doi:10.2307/2275375 |
| [61] | ORŁOWSKA E., Philosophical Logic in Poland pp 167– (1994) · doi:10.1007/978-94-015-8273-5_11 |
| [62] | ORŁOWSKA E., Time and Logic – A Computational Approach pp 249– (1995) |
| [63] | ORŁOWSKA E., Proof Theory of Modal Logic 2 pp 55– (1996) · doi:10.1007/978-94-017-2798-3_5 |
| [64] | ORŁOWSKA E., Advances in Computing Science, chapter 6, in: Relational Methods in Computer Science pp 90– (1997) · doi:10.1007/978-3-7091-6510-2_6 |
| [65] | ORŁOWSKA E., Logic, Methodology and Philosophy of Science. Proceedings of the 12th International Congress pp 147– · Zbl 0566.68037 |
| [66] | VAN DE POL J., Proceedings of MFCS, vol. 3618 of LNCS pp 769– |
| [67] | POSEGGA J., GWAI, vol. 671 of LNCS pp 67– (1992) |
| [68] | POSEGGA J., Journal of Logic and Computation 5 (6) pp 697– (1995) · Zbl 0845.68095 · doi:10.1093/logcom/5.6.697 |
| [69] | POSEGGA J., Implementing Semantic Tableaux (1999) · Zbl 0972.68519 · doi:10.1007/978-94-017-1754-0_10 |
| [70] | RASIOWA H., The Mathematics of Metamathematics (1963) · Zbl 0122.24311 |
| [71] | SCHÖNFELD W., Zeitschrift fuer Mathematische Logic und Grundlagen der Mathematik 28 pp 239– (1982) · Zbl 0506.03001 · doi:10.1002/malq.19820281408 |
| [72] | SCHNEIDER K., Formal Methods in System Design 5 (1) pp 145– (1994) · Zbl 0808.03006 · doi:10.1007/BF01384237 |
| [73] | SCHÜTZ H., Information and Computation 162 (1) pp 138– (2000) · Zbl 1045.68605 · doi:10.1006/inco.1999.2863 |
| [74] | SINZ C., Proceedings of the 17th International Conference on Automated Deduction, vol. 1831 of LNCS pp 177– |
| [75] | SMULLYAN R. M., First-Order Logic (1995) · Zbl 0172.28901 |
| [76] | TARSKI A., A Formalization of Set Theory without Variables, vol. 41 of Colloquium Publications · Zbl 0654.03036 |
| [77] | WEGENER I., Discrete Applied Mathematics 138 (1) pp 229– (2004) · Zbl 1045.94023 · doi:10.1016/S0166-218X(03)00297-X |
| [78] | WUNDERWALD J. E., Proceedings of 5th LOPSTR, vol. 1048 of LNCS pp 17– |
| [79] | Web repository of computational tools for non-Classical logics, AiML |
| [80] | Web reference for SICStus Prolog |
| [81] | ZANTEMA H., Journal of Logic and Algebraic Programing 49 (1) pp 61– (2001) · Zbl 1015.68086 · doi:10.1016/S1567-8326(01)00013-3 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
