Fuzzy Proof Logic

Here is an implementation of Fuzzy Proof Logic.

To assign a certainty degree to an axiom, type the value of this degree before the axiom, for example :

? 0.6 (foo = bar).

The proof  : 0.600 (foo = bar)
reduces to : 0.600 (foo = bar)
and proves : foo
equals     : bar
certainty  : 0.600

When two proofs are combined, the certainty degrees are multiplied :

? 0.6 (foo = bar) ; 0.5 (foo = baz).

The proof  : 0.600 (foo = bar) ; 0.500 (foo = baz)
reduces to : 0.600 (foo = bar) ; 0.500 (foo = baz)
and proves : bar
equals     : baz
certainty  : 0.300

If no certainty degree is indicated, it is assumed to be 1 :

? (mother = mom) 0.8 (Anthony = Tony).

The proof  : (mother = mom) 0.800 ((Anthony = Tony))
reduces to : (mother = mom) 0.800 ((Anthony = Tony))
and proves : mother Anthony
equals     : mom Tony
certainty  : 0.800

Here are some examples of fuzzy proofs :

? parent Anthony 0.9(mother Anthony = Brenda) ; $([parent * (mother *) = true] Anthony).

The proof  : parent Anthony 0.900 ((mother Anthony = Brenda)) ; $([parent * (mother *) = true] Anthony)
reduces to : parent Anthony 0.900 ((mother Anthony = Brenda)) ; $(parent Anthony (mother Anthony) = true)
and proves : parent Anthony Brenda
equals     : true
certainty  : 0.900

? $((child = [[parent * '*]]) Brenda Anthony) ; parent Anthony 0.9(mother Anthony = Brenda) ; $([parent * (mother *) = true] Anthony).

The proof  : ( $((child = [[parent * '*]]) Brenda Anthony) ; parent Anthony 0.900 ((mother Anthony = Brenda)) ) ; $([parent * (mother *) = true] Anthony)
reduces to : ( $((child = [[parent * '*]]) Brenda Anthony) ; parent Anthony 0.900 ((mother Anthony = Brenda)) ) ; $(parent Anthony (mother Anthony) = true)
and proves : child Brenda Anthony
equals     : true
certainty  : 0.900