# 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.

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