The universe of propositional approximations. (English) Zbl 1088.68162
Summary: The idea of approximate entailment has been proposed by M. Schaerf and M. Cadoli [Artif. Intell. 74, 249–310 (1995; Zbl 1014.03512)] as a way of modelling the reasoning of an agent with limited resources. In that framework, a family of logics, parameterised by a set of propositional letters, approximates classical logic as the size of the set increases.
The original proposal dealt only with formulas in clausal form, but in [M. Finger and R. Wassermann, J. Log. Comput. 14, 179–204 (2004; Zbl 1101.68086)], one of the approximate systems was extended to deal with full propositional logic, giving the new system semantics, an axiomatisation, and a sound and complete proof method based on tableaux. In this paper, we extend another approximate system by Schaerf and Cadoli, presented in a subsequent work [M. Cadoli and M. Schaerf, Ann. Math. Artif. Intell. 18, 29–50 (1996; Zbl 0890.03010)] and then take the idea further, presenting a more general approximation framework of which the previous ones are particular cases, and show how it can be used to formalise heuristics used in theorem proving.
The original proposal dealt only with formulas in clausal form, but in [M. Finger and R. Wassermann, J. Log. Comput. 14, 179–204 (2004; Zbl 1101.68086)], one of the approximate systems was extended to deal with full propositional logic, giving the new system semantics, an axiomatisation, and a sound and complete proof method based on tableaux. In this paper, we extend another approximate system by Schaerf and Cadoli, presented in a subsequent work [M. Cadoli and M. Schaerf, Ann. Math. Artif. Intell. 18, 29–50 (1996; Zbl 0890.03010)] and then take the idea further, presenting a more general approximation framework of which the previous ones are particular cases, and show how it can be used to formalise heuristics used in theorem proving.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
| 03B60 | Other nonclassical logic |
| 68T27 | Logic in artificial intelligence |
| 68T30 | Knowledge representation |
Keywords:
Automated reasoning; Deductive systems; Approximate reasoning; Non-classical logics; Knowledge representationReferences:
| [1] | Anderson, A.; Belnap, N., Entailment: The Logic of Relevance and Necessity, Vol. 1 (1975), Princeton University Press: Princeton University Press NJ · Zbl 0323.02030 |
| [2] | K. Broda, M. Finger, KE-tableaux for a fragment of linear logic, in: Proc. Fourth Internat. Workshop on Analytic Tableaux and Related Methods, Koblenz, 1995.; K. Broda, M. Finger, KE-tableaux for a fragment of linear logic, in: Proc. Fourth Internat. Workshop on Analytic Tableaux and Related Methods, Koblenz, 1995. |
| [3] | Broda, K.; Finger, M.; Russo, A., Labelled natural deduction for substructural logics, Logic J. IGPL, 7, 3, 283-318 (1999) · Zbl 0929.03059 |
| [4] | M. Cadoli, Semantical and computational aspects of Horn approximations, in: Proc. 13th Internat. Joint Conf. Artificial Intelligence (IJCAI-93), 1993, pp. 39-44.; M. Cadoli, Semantical and computational aspects of Horn approximations, in: Proc. 13th Internat. Joint Conf. Artificial Intelligence (IJCAI-93), 1993, pp. 39-44. |
| [5] | Cadoli, M.; Scarcello, F., Semantical and computational aspects of Horn approximations, Artif. Intell., 119, 1-2, 1-17 (2000) · Zbl 0945.68160 |
| [6] | M. Cadoli, M. Schaerf, Approximation in concept description languages, in: Proc. Third Internat. Conf. on Principles of Knowledge Representation and Reasoning (KR92), 1992, pp. 330-341.; M. Cadoli, M. Schaerf, Approximation in concept description languages, in: Proc. Third Internat. Conf. on Principles of Knowledge Representation and Reasoning (KR92), 1992, pp. 330-341. |
| [7] | Cadoli, M.; Schaerf, M., The complexity of entailment in propositional multivalued logics, Ann. Math. Artif. Intell., 18, 1, 29-50 (1996) · Zbl 0890.03010 |
| [8] | Chang, C.; Lee, R., Symbolic Logic and Mechanical Theorem Proving (1973), Academic Press: Academic Press London · Zbl 0263.68046 |
| [9] | Chopra, S.; Parikh, R.; Wassermann, R., Approximate belief revision, Logic J. IGPL, 9, 6, 755-768 (2001) · Zbl 1005.03020 |
| [10] | D’Agostino, M., Are tableaux an improvement on truth-tables?—cut-free proofs and bivalence, J. Logic Language Inform., 1, 235-252 (1992) · Zbl 0793.03059 |
| [11] | D’Agostino, M.; Gabbay, D., A generalization of analytic deduction via labelled tableaux, part I: basic substructural logics, J. Automated Reason., 13, 243-281 (1994) · Zbl 0816.03012 |
| [12] | M. Dalal, Anytime families of tractable propositional reasoners, in: Internat. Symp. of Artificial Intelligence and Mathematics AI/MATH-96, 1996, pp. 42-45.; M. Dalal, Anytime families of tractable propositional reasoners, in: Internat. Symp. of Artificial Intelligence and Mathematics AI/MATH-96, 1996, pp. 42-45. |
| [13] | M. Dalal, Semantics of an anytime family of reasoners, in: 12th European Conference on Artificial Intelligence, 1996, pp. 360-364.; M. Dalal, Semantics of an anytime family of reasoners, in: 12th European Conference on Artificial Intelligence, 1996, pp. 360-364. |
| [14] | W. Dias, Tableaux implementation for approximate reasoning (in portuguese), Master’s Thesis, Department of Computer Science, University of São Paulo, 2002.; W. Dias, Tableaux implementation for approximate reasoning (in portuguese), Master’s Thesis, Department of Computer Science, University of São Paulo, 2002. |
| [15] | M. Finger, Polynomial approximations of full propositional logic via limited bivalence, in: Ninth European Conference on Logics in Artificial Intelligence (JELIA 2004), Lecture Notes in Artificial Intelligence, Vol. 3229, Springer, Lisbon, Portugal, 2004, pp. 526-538.; M. Finger, Polynomial approximations of full propositional logic via limited bivalence, in: Ninth European Conference on Logics in Artificial Intelligence (JELIA 2004), Lecture Notes in Artificial Intelligence, Vol. 3229, Springer, Lisbon, Portugal, 2004, pp. 526-538. · Zbl 1111.68675 |
| [16] | M. Finger, Towards polynomial approximations of full propositional logic, in: A.L.C. Bazzan, S. Labidi (Eds.), XVII Brazilian Symposium on Artificial Intelligence (SBIA 2004), Lecture Notes in Artificial Intelligence, Vol. 3171, Springer, Berlin, 2004, pp. 11-20.; M. Finger, Towards polynomial approximations of full propositional logic, in: A.L.C. Bazzan, S. Labidi (Eds.), XVII Brazilian Symposium on Artificial Intelligence (SBIA 2004), Lecture Notes in Artificial Intelligence, Vol. 3171, Springer, Berlin, 2004, pp. 11-20. · Zbl 1105.68101 |
| [17] | M. Finger, R. Wassermann, Approximate reasoning and paraconsistency, in: Eighth Workshop on Logic, Language, Information and Computation (WoLLIC’2001), 2001, pp. 77-86.; M. Finger, R. Wassermann, Approximate reasoning and paraconsistency, in: Eighth Workshop on Logic, Language, Information and Computation (WoLLIC’2001), 2001, pp. 77-86. |
| [18] | M. Finger, R. Wassermann, Tableaux for approximate reasoning, in: L. Bertossi, J. Chomicki, (Eds.), IJCAI-2001 Workshop on Inconsistency in Data and Knowledge, Seattle, 2001, pp. 71-79.; M. Finger, R. Wassermann, Tableaux for approximate reasoning, in: L. Bertossi, J. Chomicki, (Eds.), IJCAI-2001 Workshop on Inconsistency in Data and Knowledge, Seattle, 2001, pp. 71-79. |
| [19] | Finger, M.; Wassermann, R., Expressivity and control in limited reasoning, (van Harmelen, F., 15th European Conference on Artificial Intelligence (ECAI02) (2002), IOS Press: IOS Press Lyon, France), 272-276 |
| [20] | M. Finger, R. Wassermann, Logics for approximate reasoning: approximating classical logic “from above”, in: XVI Brazilian Symposium on Artificial Intelligence (SBIA’02), Lecture Notes in Artificial Intelligence, Vol. 2507, Springer, Berlin, 2002, pp. 21-30.; M. Finger, R. Wassermann, Logics for approximate reasoning: approximating classical logic “from above”, in: XVI Brazilian Symposium on Artificial Intelligence (SBIA’02), Lecture Notes in Artificial Intelligence, Vol. 2507, Springer, Berlin, 2002, pp. 21-30. · Zbl 1031.68115 |
| [21] | Finger, M.; Wassermann, R., Approximate and limited reasoning: semantics, proof theory, expressivity and control, J. Logic Comput., 14, 2, 179-204 (2004) · Zbl 1101.68086 |
| [22] | H. Levesque, A logic of implicit and explicit belief, in: Proc. AAAI-84, 1984, pp. 198-202.; H. Levesque, A logic of implicit and explicit belief, in: Proc. AAAI-84, 1984, pp. 198-202. |
| [23] | F. Massacci, Efficient approximate deduction and an application to computer security, Ph.D. Thesis, Dottorato in Ingegneria Informatica. Università di Roma I “La Sapienza”, Dipartimento di Informatica e Sistemistica, 1998. URL \(\langle;\) http://www.ing.unitn.it/\( \sim;\rangle;\); F. Massacci, Efficient approximate deduction and an application to computer security, Ph.D. Thesis, Dottorato in Ingegneria Informatica. Università di Roma I “La Sapienza”, Dipartimento di Informatica e Sistemistica, 1998. URL \(\langle;\) http://www.ing.unitn.it/\( \sim;\rangle;\) |
| [24] | D. McAllester, Truth maintenance, in: Proc. Eighth National Conf. on Artificial Intelligence (AAAI-90), 1990, pp. 1109-1116.; D. McAllester, Truth maintenance, in: Proc. Eighth National Conf. on Artificial Intelligence (AAAI-90), 1990, pp. 1109-1116. |
| [25] | Schaerf, M.; Cadoli, M., Tractable reasoning via approximation, Artificial Intelligence, 74, 2, 249-310 (1995) · Zbl 1014.03512 |
| [26] | B. Selman, H. Kautz, Knowledge compilation using Horn approximations, in: Proc. AAAI-91, 1991, pp. 904-909.; B. Selman, H. Kautz, Knowledge compilation using Horn approximations, in: Proc. AAAI-91, 1991, pp. 904-909. |
| [27] | Selman, B.; Kautz, H., Knowledge compilation and theory approximation, J. ACM, 43, 2, 193-224 (1996) · Zbl 0882.68137 |
| [28] | Smullyan, R. M., First-Order Logic (1968), Springer: Springer Berlin · Zbl 0172.28901 |
| [29] | A. ten Teije, F. van Harmelen, Computing approximate diagnoses by using approximate entailment, in: Proc. of KR’96.; A. ten Teije, F. van Harmelen, Computing approximate diagnoses by using approximate entailment, in: Proc. of KR’96. |
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.
