Decision Procedures and Model Building for Fuzzy Logics

01.07.2003 - 30.11.2005
Assigned research project
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 uzzy logic is needed for an adequate treatment of such important topics as {\em formalizing} ubiquitious natural language predicates (like: tall(x), dark(x), likes(x,y) etc.), representing fuzzy knowlegde of different kinds, and reasoning with fuzzy and vague concepts. 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.

People

Project leader

Project personnel

Institute

Contract/collaboration

  • FWF, Der Wissenschaftsfonds

Keywords

GermanEnglish
Fuzzy-Logikfuzzy logic
automatische Modellbildungauotmated model building
Entscheidungsverfahrendecision procedures

Publications