Internet-Publication. — 10 p. English. (OCR-слой).[Reiner Hahnle. University of Karlsruhe. Institute for Logic, Complexity and Deduction Systems. Karlsruhe, Germany].Abstract.
This paper tries to identify the basic problems encountered in automated theorem proving in many-valued logics and demonstrates to which extent they can be currently solved. To this end a number of recently developed techniques are reviewed. We list the avenues of research in many-valued theorem proving that are in our eyes the most promising.Introduction.
The purpose of this note is to review a number of techniques that lead to a computationally adequate representation of the search space of many-valued logics and to identify the avenues of research in many-valued theorem proving that are in our eyes the most promising. We do not mention the large number of possible applications of many-valued theorem proving, but refer to [15] for an extensive list of applications and to [18] for a case study.
If one is doing many-valued deduction, typically a number of problems that are not as much prominent in classical deduction have to be addressed:
The number of case distinctions is much larger due to the increased number of truth values.
The amount of redundancy in deductions is much bigger. Typically, many-valued connectives show a certain degree of regularity and one has to nd ways of how to exploit this.
In general, internal normal forms (that is, normal forms based solely on connectives from the logic under consideration) are not available.
In the case of infinitely-valued logics there is the problem to find a finite representation of the search space.Introduction.
Many-Valued Logic.
Definition - (Syntax).
Definition - (Truth Values, Semantic, Logic).
Definition - (Valuation).
Definition - (S-Satisfiability, -Consequence).
Definition - (First-Order Syntax).
Definition - (First-Order Semantics/Logic).
Example - Lukasiewicz Logics.
Sets as Signs.
Definition - (Signed Formula).
Regular Logics.
Definition - (Circle, Corner [13]).
Definition - (Regular Logic [13]).
Definition - (Partially Ordered Set).
Definition - (Up-, Downset).
Normal Forms.
Resolution, parallel version: Definition - (Signed Subsumption).
Integer Programming.
Implementation.
Conclusion and Outlook.
References (30 publ.).
