Decision Procedures and Model Building for Fuzzy Logics

Automated Reasoning is often considered only in the narrow sense of providing programs that search for proofs of valid formulas. However, most applications of automated reasoning require systems that, in addition, also aim at the following features: 1. The theorem prover should terminate---for large, syntactically characterized classes of formulas---also if no proof of the input formula exists. 2. If the input formula is not provable, the system should (if possible) provide a description of a counter-model of this formula as output. The closely related areas of proof search based decision procedures and automated model building address these two research tasks, respectively. Substantial progress for classical clause logic has already been achieved in both areas. However, the---often almost exclusive---focus on classical logic, especially in automated model building, is at variance with the increasing importance of non-classical logics in many fields of computer science. In particular, it is well known that classical (two-valued) logic is ill-equipped for formalizing reasoning with vague concepts and information. It is widely recognized that the more complex machinery of fuzzy logic is needed for an adequate treatment of such important topics as formalizing ubiquitious natural language predicates (like: tall(x), dark(x), likes(x,y) etc.), representing inexact knowlegde of different kinds, and reasoning with fuzzy and vague concepts. Only in recent years, a sound and mathematically mature foundation of deduction in fuzzy logics is emerging. The task of automated reasoning in fuzzy contexts is one that calls for systems that support not only proof search, but also provide decision procedures and are able to output information about counter-models in case of failed proof search. Consequently, we aim at the devlopment of proof search based decision procedures and model building algorithms for the most relevant fuzzy logics. The research will lead us to investigate analogous problems also for related logics; in particular for families of finite valued logics that allow to approximate reasoning tasks referring to (infinite valued) fuzzy logics.

Fuzzy logics are mathematical tools for modeling formal reasoning with vague information and concepts. Especially the rapid increase of importance of the Internet as almost universal, but mainly natural language oriented and therefore often vague source of information explains the interest in mathematical results about fuzzy logics. Particular attention is paid to algorithms, so-called decision procedures, that allow to detect automatically whether logical consequence relations hold between given formulas of the corresponding target logics. In this project proof search formalisms for some of the most important fuzzy logics have been developed and analyzed with respect to their use as decision procedures. As a main result a special calculus has been designed, which - for the first time - allows to find formal, analytic proofs for the three fundamental t-norm based fuzzy logics (Lukasiewicz logic, Gödel logic, and Product logic) in a uniform manner. This calculus moreover enjoys a number of favorable properties, which render it a useful base for decision procedures. In particular, variants of the calculus have been shown to be of optimal computational complexity. In addition to the mentioned decision procedures the following problem was tackled successfully: when a complete (fuzzy logical) deduction system terminates without finding a proof, what information about concrete counter models can be extracted from proof search? Detailed answers could be provided for Gödel logic, which is probably the simplest logic that formalizes the idea that propositions, in general, are not always just either definitely false or definitely true, but rather can be ordered and compared with respect to arbitrary degrees of their respective truth. As a further focus of obtained results, formal dialogue games have been analyzed that show a close correspondence to the above mentioned analytic proof systems. Those games allow to model the systematic processing of logically complex, but vague information. In this context it emerged that a number of competing concepts and theories of vagueness have to be taken into account. The systematic analysis of corresponding dialogue games will be a main tool in future investigations addressing this challenge.