Logic Journal of IGPL Advance Access originally published online on November 17, 2008
Logic Journal of IGPL 2008 16(6):537-560; doi:10.1093/jigpal/jzn020
Cut-Based Abduction
In this paper we explore a generalization of traditional abduction which can simultaneously perform two different tasks: (i) given an unprovable sequent 
G, find a sentence H such that , H G is provable (hypothesis generation); (ii) given a provable sequent G, find a sentence H such that H and the proof of , H G is simpler than the proof of G (lemma generation). We argue that the two tasks should not be distinguished, and present a general procedure for finding suitable hypotheses or lemmas. When the original sequent is provable, the abduced formula can be seen as a cut formula with respect to Gentzen's sequent calculus, so the abduction method is cut-based. Our method is based on the tableau-like system KE and we argue for its advantages over existing abduction methods based on traditional Smullyan-style Tableaux.
Received for publication 8 September 2008.
*Partly supported by CNPq grant PQ 301294/2004-6 and FAPESP project 04/14107-2.
References
-
1 Aliseda-Llera Atocha. Seeking explanations: abduction in logic, philosophy of science and artificial intelligence (1997) Stanford, CA, USA: Stanford University. PhD thesis.
2 Boolos George. Donh't eliminate cut. Journal of Philosophical Logic (1984) 13:373–378.
3 Buss Samuel R. Some remarks on lengths of propositional proofs. Archive for Mathematic Logic (1995) 34:377–394.[CrossRef]
4 Carbone Alessandra, Semmes Stephen. A Graphic Apology for Symmetry and Implicitness (2000) Oxford Mathematical Monographs. Oxford University Press.
5 Carnielli Walter. Surviving abduction. Logic Journal of IGPL (2006) 14(2):237–256.
6 Mayer Marta Cialdea, Pirri Fiora. First-order abduction via tableau and sequent calculi. Journal of the IGPL (1993) 1(1):99–117.[CrossRef]
7 Mayer Marta Cialdea, Pirri Fiora. Modal propositional abduction. Journal of the IGPL (1995) 3(6):99–117.
8 Mayer Marta Cialdea, Pirri Fiora. Abduction is not deduction-in-reverse. Journal of the IGPL (1996) 41(1):95–108.
9 Colucci Simona, Di Noia Tommaso, Di Sciascio Eugenio, Donini Francesco M, Mongiello Marina. A uniform tableaux-based approach to concept abduction and contraction in aln. In. Description Logics (2004).
10 D’Agostino Marcello. Are tableaux an improvement on truth-tables? — Cut-free proofs and bivalence. Journal of Logic, Language and Information (1992) 1:235–252.[CrossRef]
11 D’Agostino Marcello. Tableau methods for classical propositional logic. In. In: Handbook of Tableau Methods—D’Agostino Marcello, Gabbay Dov, Haehnle Rainer, Posegga Joachim, eds. (1999) Kluwer. 45–124.
12 D’Agostino Marcello, Mondadori Marco. The taming of the cut. Classical refutations with analytic cut. Journal of Logic and Computation (1994) 4(285–319).
13 Demolombe Robert, Fariñas del Cerro Luis. An inference rule for hypothesis generation. In. In: Proceedings of IJCAI (1991) 152–157.
14 Finger Marcelo, Gabbay Dov. Cut and pay. Journal of Logic, Language and Information (2006) October;15(3):195–218.[CrossRef]
15 Gabbay Dov, Woods John. The Reach of Abduction: Insight and Tria (2005) volume 2. Elsevier. volume A Practical Logic of Cognitive Systems.
16 Gabbay Dov, Woods John. Advice on abductive logic. Logic Journal of the IGPL (2006) March;14(2):189–219(31).[CrossRef][Web of Science]
17 Letz Reinhold, Stenz Gernot. The disconnection tableau calculus. Journal of Automated Reasoning (2007) 38(1-3):79–126.[CrossRef][Web of Science]
18 Sanders Peirce Charles. Collected Papers of Charles Sanders Peirce—Hartshorne Charles, Weiss Paul, Burks Arthur, eds. (1931–1958) 1–8. Harvard University Press.
19 Poole David. Representing knowledge for logic-based diagnosis. (1988) 1282–1290. In Proceedings of the International Conference on Fifth Generation Computer Systems.
20 Reiter Raymond, de Kleer Johan. Foundations of assumption-based truth maintenance systems: Preliminary report. In. In: AAAI (1987) 183–189.
21 Shanahan Murray. Prediction is deduction but explanation is abduction. In. In: Proceedings of IJCAI (1989) 1055–1060.
22 Smullyan Raymond M. First-Order Logic (1968) Springer-Verlag.
23 Tseitin GS. On the complexity of derivations in the propositional calculus. In. In: Structures in Constructive Mathematics and Mathematical Logic, Part II—Slisenko AO, ed. (1968) New-York-London: Consultants Bureau. 115–125. Translated from Russian.
CiteULike 
Connotea 
Del.icio.us What's this?
| ||||||||||||||||||||||||||||||||||||||||||||||||||