Abstract

The SCHEMATA functional programming language for writing deduction systems is proposed and its applications in the construction of a Nonmonotonic Reasoning System are illustrated. SCHEMATA implements deduction as a less controlled form of computation by rewriting expressions under equivalence preservation. It approaches the representation and application of deductive knowledge using the lambda-abstraction and the lambda-conversion mechanisms of SCHEME properly modified by: equivalence preservation during evaluation, a pattern matching sublanguage on the argument expression of functions, multiple expressions, with emptiness representing failure, as the result of any expression evaluation, and a complete backtracking mechanism which homogeneously controls the search required by the pattern matching process and the multiple solutions generated by each subexpression. ;In addition to variables, the pattern matching sublanguage includes constants, ellipses, schemators, and complex expressions. Symbols can have associated multiple values representing rules of deduction with the association of the symbol to itself as the natural way of reflecting its normal form. Consequently, function application is discriminated by pattern matching over expressions of the same language. Disregarding the pattern matching sublanguage and some utilitarian functions for constructing deductive systems, only two primitive operations are aggregated to SCHEME: join and split. These nondeterministic primitives show the language suitability for parallelism. ;The NRS demonstrates SCHEMATA's suitability for arbitrary deductive operations. The NRS solves equations and simplifies expressions in the Z Modal Logic not only producing the predicted results of several different theories of Nonmonotonic Reasoning including Moore's Autoepistemic Logic, Nonconstructive Default Logic, Reiter's Default Logic, the Closed World Assumption, McCarthy's Parallel Circumscription, and Levesque's BNO, but also solving other problems not representable in those theories. The NRS implementation is amply discussed and an example diagnosing circuit devices is presented. References to applications of NRS in Physics, Diagnosis, Deontic Reasoning, Situation Calculus, Event Calculus, Assembling, Manufacturing and Planning are included. The document also contains a Sequent Logic theorem prover for Number Theory implemented in SCHEMATA