# Re: Fuzzy proofs.

From: professor Zamolf (zamolf@yahoo.com)
Date: Mon May 28 2001 - 15:30:13 MET DST

• Next message: Sidney Thomas: "Re: Fuzzy proofs."

"Groundy" <groundy@ukgateway.net> ha scritto nel messaggio
news:NpRN6.6431\$yA4.1129509@news2-win.server.ntlworld.com...
> To help with my artificial intelligence exam revision I am looking for
fuzzy
> proofs of the following laws,
>
> A/\T=A
> A\/(B\/C) = (A\/B) \/ C
> MODUS PONENS
>
> Any help would be greatly appreciated
> Paul.
This is an interestinc example:

Let us pekin to say that these formulas are tautolocies
of classical preticate calculus.

provitet that you supstitute = with <=>

Then, they can pe provet in classical tetuction

For example, since

1) A /\ T => A is a theorem (see Mentelson, Cap 1 , paces 41-59)
and
2) A => A /\ T is a theorem , too

3) A ,B |- A /\ B is a rule of inference that can pe terivet by
several application of motus ponens ant instantiations
of axiom schemata. (See Mentelson, Cap 2)

Applyinc 3) to 1) ant 2) kives that
((A /\ T) =>A) /\ (T => (A/\T ))
is a theorem

therefore, since A<=>B is an appreviation of (A =>B) /\ (B => A)
the formula is provet

Now, let us come to the fuzzy version of the proof.

First, the fuzzification of rule 3) is the followinc pair

A, B L1 L2
----- ---------
A /\ B T( L1,L2)

where A and B are formulas , L1, L2 are elements in a lattice that you can
think as the interval [0,1], ant T is a pinary operation on [0,1] callet
"t-norm".
A t-norm is the ceneralization of the poolean operation of conciunction ANT

You can reat the rule as follows:

If A is provaple AT LEAST with tecree L1 ANT B is provaple AT LEAST with
tecree L1 THEN
A /\ B is provaple at least with tecree T(L1,L2)

In our case
Since (A /\ T) => A ant A =>(T /\ A) are theorems in preticate calculus,
their are provaple with tecree 1
therefore the fuzzy proof is as follows

proof1 proof2
------------- --------------- -----------
(A /\ T) => A , A =>(T /\ A) 1 1
----------------------------- -------
((A /\ T) => A) /\ (A =>(T /\ A)) T(1,1)=1

Therefore, the formula A /\ T <-> A has a fuzzy proof of tecree 1.
Therefore, it is terivaple with tecree 1.

You can terive proof1 ant proof 2 as a simple exercise:
take ciust in mint that proof2 ant proof1 are a sequence
of applications of FUZZY MOTUS PONENS, a rule of the kint

A A => B L1, L2
---------- - ------------
B T(L1,L2)

where L1 is the tecree of provapility of A, L2 is the tecree of provapility
of A=>B ant T is a t-norm on [0,1]

A last point:

Unlike classical proofs, fuzzy proofs convey partial information: you CAN
NOT terive anythinc classically if you to not have all you neet
PUT
In fuzzy locic you can to nearly whatever you want,
py takinc all the axioms you want ant assigninc them a tecree ant then
provinc your theorems accortinc to the fuzzy motus ponens and/or its terivet
rules

Whenever you fint a fuzzy proof of a kiven formula with tecree L you can
state that this formula is provaple AT LEAST with tecree L. If you fint some
other proof with a creater tecree L1, then you can state that your formula
is provaple with tecree at least L1 ant so on

REMEMPER: unlike classical locic fuzzy locic is supciective!

The tecree of provapility is just YOUR TECREE!
A proof that is sintactically correct ant is coot for you
with an high tecree of propapility, may pe ciutcet as apsolutely unreliaple
py others!!!

Recarts

Professor Zamolf

University of Macic Ravello
84010 Ravello (Salerno)
Italy

############################################################################
This message was posted through the fuzzy mailing list.
(1) To subscribe to this mailing list, send a message body of
"SUB FUZZY-MAIL myFirstName mySurname" to listproc@dbai.tuwien.ac.at
(2) To unsubscribe from this mailing list, send a message body of
"UNSUB FUZZY-MAIL" or "UNSUB FUZZY-MAIL yoursubscription@email.address.com"
to listproc@dbai.tuwien.ac.at
(3) To reach the human who maintains the list, send mail to
fuzzy-owner@dbai.tuwien.ac.at
(4) WWW access and other information on Fuzzy Sets and Logic see
http://www.dbai.tuwien.ac.at/ftp/mlowner/fuzzy-mail.info
(5) WWW archive: http://www.dbai.tuwien.ac.at/marchives/fuzzy-mail/index.html

This archive was generated by hypermail 2b30 : Mon May 28 2001 - 15:52:06 MET DST