First-order logic in practice, how to deal with undecidability?

I am very new to these things. Hopefully this is not a very naive question.

I tried the following formula in Prolog: A ⇒ B

and given that B is true, I evaluate A and it says FALSE.

My question is why FALSE? (why not TRUE?) Given the current information, we do not know anything about Bed and . Does Prolog work on the assumption that for something unknown, it outputs FALSE?

If that's the assumption, how common is it?

Another thing that comes to mind is that it finds an assignment to connect input queries and axioms (mostly SAT solutions). Since the resulting result is TRUE, no matter what the value of A is , it just picks one random (or zero by default?).

Based on the properties of 1st order logic, it is semi-decidable. if clause A logically implies clause B , then this can be found, but not vice versa. So how is the latter case handled in practice when there is no evidence of TRUTH?

PS1. A little explanation of how Prolog works may also be helpful. Does SAT use solvers as a black box? Or greedy search algorithms?

enter image description here

+3


source to share


3 answers


Does Prolog work on the assumption that it outputs FALSE for something unknown?

Yes of course. This behavior reflects Closed Assumption (CWA) in the sense that if a fact is not explicitly stated, it is considered false.

If that's the assumption, how common is it?



Very often - most databases use this assumption.

It might help you to know about Prolog output method: SLD resolution .

+2


source


To reason about uncertainty in Prolog, you can write an interpreter for three-valued logic . In this interpreter, truth values true

, false

and unknown

:

:- initialization(main).
main :-
    three_valued_logic(((true,false);unknown),Result),
    writeln(Result).

three_valued_logic(true,true).
three_valued_logic(false,false).
three_valued_logic(unknown,unknown).
three_valued_logic(not(A),false) :-
    three_valued_logic(A,true).
three_valued_logic(not(A),true) :-
    three_valued_logic(A,false).
three_valued_logic(not(A),unknown):-
    three_valued_logic(A,unknown).
three_valued_logic((A,B),true) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==true;B1==true).
three_valued_logic((A,B),false) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==false;B1==false).
three_valued_logic((A,B),unknown) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==unknown;B1==unknown).
three_valued_logic((A;B),unknown) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==unknown;B1==unknown),(A1==false;B1==false).
three_valued_logic((A;B),false) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==false,B1==false).
three_valued_logic((A;B),true) :-
    three_valued_logic([A,B],[A1,B1]),
    (A1==true;B1==true).
three_valued_logic([],[]).
three_valued_logic([A|B],[A1|B1]) :-
    three_valued_logic(A,A1),three_valued_logic(B,B1).

      



In this example, the value is ((true,false);unknown)

unknown,

then as (false,unknown)

equal false

.

0


source


Pure Prolog does not use a closed world guess. So if you get a "false" or "no" answer, it means NOT PERFORMANCE. Or it is written symbolically:

The value "false" or "no" in a pure prologue:

~ (Database |- Query)              (i)

      

This does not mean that Query negation is deducible. Therefore, the answer "false" or "no" does not mean symbolically:

Invalid value for "false" or "not" in pure prologue:

Database |- ~Query                 (ii)

      

There are some operators, such as negation as rejection (+) / 1, which allow the Prolog interpreter to move from (i) to (ii). But this is no longer pure Prolog, and under the hood, for example (+) / 1 can be implemented using illogical operators such as the cut (!).

Yes, cut (!) Is no longer pure Prolog, nor is it declarative. For example, negation as failure (+) / 1 is done like this:

\+ X  :- X, !, fail.
\+ _.

      

Denial as failure has problems such as shifting the value depending on whether arguments are used or not. There are other ways to add negative knowledge to Prolog programs, but you cannot find them in regular Prologs, as they are more complex than the cut (!) Method.

Bye

-1


source







All Articles