Computational aspects of three-valued logic. (English) Zbl 0644.03015

Schmitt, P. H.

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)

Keywords:

three-valued logic; natural language semantics; complete proof system; negative resolution; Horn clauses; PROLOG-style proof procedure

Citations:

Zbl 0598.00015