A tableaux-based theorem prover for a decidable subset of default logic
作者： Camilla B. Schwind
DOI: 10.1007/3-540-52885-7_112
关键词:
摘要: We present a new, efficient and clear method for computing extensions deriving formulas of normal default theory which offers new insight into the nature reasoning seems to be equally successfully applicable open non-normal theories. It is based on semantic tableaux (Smullyan 1968) works theories with finite set defaults are formulated over decidable subset first-order logic. prove that all can produced by constructing tableau one formula built from general laws consequences.
springer.com
sci-hub.st 参考文章(9)
Rene Quiniou, Patrice Quinton, Philippe Besnard, A theorem-prover for a decidable subset of default logic national conference on artificial intelligence. pp. 27- 30 ,(1983)
Camilla Schwind, Emmanuel Lafon, A theorem prover for action performance european conference on artificial intelligence. pp. 541- 546 ,(1988)
Raymond M. Smullyan, First-Order Logic ,(1968)
Philippe Besnard, Pierre Siegel, Supposition-Based Logic for Automated Nonmontonic Reasoning conference on automated deduction. pp. 592- 601 ,(1988) , 10.1007/BFB0012860
Frank M. Brown, A commonsense theory of nonmonotonic reasoning conference on automated deduction. pp. 209- 228 ,(1986) , 10.1007/3-540-16780-3_92
Genevieve Bossu, Pierre Siegel, Saturation, nonmonotonic reasoning and the closed-world assumption Artificial Intelligence. ,vol. 25, pp. 13- 63 ,(1985) , 10.1016/0004-3702(85)90040-2
R. Reiter, A logic for default reasoning Artificial Intelligence. ,vol. 13, pp. 68- 93 ,(1987) , 10.1016/0004-3702(80)90014-4
Georges Ripert, Université d'Aix-Marseille ,(1902)
Raymond R. Smullyan, First-Order Logic Springer Berlin Heidelberg. ,(1968) , 10.1007/978-3-642-86718-7