zbMATH — the first resource for mathematics

Computational aspects of three-valued logic. (English) Zbl 0644.03015
Automated deduction, Proc. 8th Int. Conf., Oxford/Engl. 1986, Lect. Notes Comput. Sci. 230, 190-198 (1986).
Summary: [For the entire collection see Zbl 0598.00015.]
This paper investigates a three-valued logic \(L_ 3\), that has been introduced in the study of natural language semantics. A complete proof system based on a three-valued analogon of negative resolution is presented. A subclass of \(L_ 3\) corresponding to Horn clauses in two- valued logic is defined. Its model theoretic properties are studied and it is shown to admit a PROLOG-style proof procedure.

03B50 Many-valued logic
03B65 Logic of natural languages
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)