A tableau calculus for Hájek’s logic BL.

*(English)*Zbl 1055.03017One of the main motivations for describing a theory in formal axiomatic terms is to make it clearer and unambiguous. The fact that the resulting theory is unambiguous often leads to another potential benefit of formalization: the ability to automate proof search in the theory.

For fuzzy logic, up to now, the main objective of its formalization was to clarify the notions. The paper under review provides, to the best of my knowledge, the first proof system for a formalized fuzzy logic, a proof system that can be, in principle, used in automatic proof search. Specifically, the authors provide a tableaux calculus for BL (Basic Logic), a formalization of fuzzy logic provided by Hájek in which there are two basic connectives \(\&\) and \(\to\) and one constant \(\bot\) (“false”). Other constants and connectives can be explicitly and naturally defined in terms of the basic ones: e.g., \(\top\) (“true”) is defined as \(\bot\to\bot\), \(\neg A\) as \(A\to\bot\), etc.

The new tableaux calculus is appropriate for automatic proofs because it is cut-free, has a subformula property, and correctness of proof can be checked in polynomial time.

For fuzzy logic, up to now, the main objective of its formalization was to clarify the notions. The paper under review provides, to the best of my knowledge, the first proof system for a formalized fuzzy logic, a proof system that can be, in principle, used in automatic proof search. Specifically, the authors provide a tableaux calculus for BL (Basic Logic), a formalization of fuzzy logic provided by Hájek in which there are two basic connectives \(\&\) and \(\to\) and one constant \(\bot\) (“false”). Other constants and connectives can be explicitly and naturally defined in terms of the basic ones: e.g., \(\top\) (“true”) is defined as \(\bot\to\bot\), \(\neg A\) as \(A\to\bot\), etc.

The new tableaux calculus is appropriate for automatic proofs because it is cut-free, has a subformula property, and correctness of proof can be checked in polynomial time.

Reviewer: Vladik Ya. Kreinovich (El Paso)