Title :
Automated reasoning with ordinary assertions and default assumptions
Author :
Van Heule, Dirk ; Hoogewijs, Albert
Author_Institution :
Dept. of Math., R. Mil. Acad., Brussels, Belgium
Abstract :
In this paper, we explain the use of PPC NAT, a three-valued first-order object logic (PPC) implemented in Isabelle, for reasoning with undefined expressions. This kind of expressions can be found in default logic where deductions are divided from facts (which are true) together with a set of assumptions (defaults), which can be true. The main features of our system are: the ability to formalize default assumptions and to reason about them automatically
Keywords :
nonmonotonic reasoning; ternary logic; Isabelle; PPC NAT; assertions; automated reasoning; default assumptions; default logic; three-valued first-order object logic; Calculus; Cost accounting; Logic design; Mathematics; Military computing; Multivalued logic;
Conference_Titel :
Multiple-Valued Logic, 2001. Proceedings. 31st IEEE International Symposium on
Conference_Location :
Warsaw
Print_ISBN :
0-7695-1083-3
DOI :
10.1109/ISMVL.2001.924572
