Did you know ... | Search Documentation: |

Well Founded Semantics |

- Documentation
- Reference manual
- Tabled execution (SLG resolution)

- Packages

- Reference manual

According to
Wikipedia,
"*Well Founded Semantics* is one definition of how we can make
conclusions from a set of logical rules". Well Founded Semantics (WFS)
defines a *three valued logic* representing *true*,
*false* and something that is neither true or false. This latter
value is often referred to as *bottom*, *undefined* or
*unknown*. SWI-Prolog uses undefined/0.

Well Founded Semantics allows for reasoning about programs with
contradictions or multiple answer sets. It allows for obtaining
true/false results for literals that do not depend on the sub program
that has no unambiguous solution, propagating the notion of
*undefined* to literals that cannot be resolved otherwise and
obtaining the *residual* program that expresses why an answer is
not unambiguous.

The notion of *Well Founded Semantics* is only relevant if the
program uses *negation* as implemented by tnot/1.
The argument of
tnot/1,
as the name implies, must be a goal associated with a tabled predicate
(see table/1).
In a nutshell, resolving a goal that implies
tnot/1
is implemented as follows:

Consider the following partial *body term*:

..., tnot(p), q.

- If
`p`has an unconditional answer in its table, fail. - Else,
*delay*the negation. If an unconditional answer arrives at some time, resume with failure. - If at the end of the traditional tabled evaluation we can still not
decide on
`p`, execute the*continuation*(`q`above) while maintaining the*delay list*set to`tnot(p)`

. If executing the continuation results in an answer for some tabled predicate, record this answer as a*conditional*answer, in this case with the condition`tnot(p)`

. - If a conditional answer is added to a table, it is propagated to its
*followers*, say`f`, adding the pair {`f`,answer} to the delay list. If this leads to an answer, the answer is conditonal on this pair. - After the continuations of all unresolved tnot/1 calls have been executed the various tables may have conditional answers in addition to normal answers.
- If there are negative literals that have neither conditional answers
nor unconditional answers, the condition
`tnot(g)`

is true. This conclusion is propagated by simplifying the conditions for all answers that depend on`tnot(g)`

. This may result in a definite*false*condition, in which case the answer is removed or a definite*true*condition in which case the answer is made unconditional. Both events can make other conditional answers definitely true or false, etc. - At the end of the simplifying process some answers may still be
conditional. A final
*answer completion*step analyses the graph of depending nodes, eliminating*positive loops*, e.g., ```p`:-`q`.`q`:-`p`''. The answers in such a loop are removed, possibly leading to more simplification. This process is executed until*fixed point*is reached, i.e., no further positive loops exist and no further simplification is possible.

The above process may complete without any remaining conditional
answers, in which case we are back in the normal Prolog world. It is
also possible that some answers remain conditional. The most obvious
case is represented by undefined/0.
The toplevel responds with
**undefined** instead of **true** if an answer is conditional.

**undefined**- Unknown represents neither
`true`

nor`false`

in the well formed model. It is implemented as:- table undefined/0. undefined :- tnot(undefined).

Solving a set of predicates under
well formed semantics results in a
*residual program*. This program contains clauses for all tabled
predicates with condition answers where each clause head represents and
answer and each clause body its condition. The condition is a
disjunction of conjunctions where each literal is either a tabled goal
or tnot/1
of a tabled goal. The remaining model has at least a cycle through a
negative literal (tnot/1)
and has no single solution in the *stable model semantics*, i.e.,
it either expresses a contradition (as undefined/0,
i.e., there is no stable model) or a multiple stable models as in the
program below, where both {p} and {q} are stable models.

:- table p/0, q/0. p :- tnot(q). q :- tnot(p).

Note that it is possible that some literals have the same truth value
in all stable models but are still *undefined* under the stable
model semantics.

The residual program is an explanation of why an answer is undefined. SWI-Prolog offers the following predicates to access the residual program.

**call_residual_program**(`:Goal, -Program`)- True when
`Goal`is an answer according to the Well Founded Semantics. If`Program`is the empty list,`Goal`is unconditionally true. Otherwise this is a program as described by delays_residual_program/2. **call_delays**(`:Goal, -Condition`)- True when
`Goal`is an answer that is true when Condition can be satisfied. If`Condition`is`true`

,`Answer`is unconditional. Otherwise it is a conjunction of goals, each of which is associated with a tabled predicate. **delays_residual_program**(`:Condition, -Program`)- Program is a list of clauses that represents the connected program
associated with
`Condition`. Each clause head represents a conditional answer from a table and each corresponding clause body is the condition that must hold for this answer to be true. The body is a disjunction of conjunctions. Each leaf in this condition is either a term`tnot(Goal)`

or a plain`Goal`. Each`Goal`is associated with a tabled predicate. The program always contains at least one cycle that involves tnot/1.

The toplevel supports two modes for reporting that it is undefined
whether the current answer is true. The mode is selected by the Prolog
flag
toplevel_list_wfs_residual_program.
If `true`

, the toplevel uses call_delays/2
and delays_residual_program/2
to find the conditional answers used and the *residual* program
associated with these answers. It then prints the residual program,
followed by the answer and the conditional answers. For undefined/0,
this results in the following output:

?- undefined. % WFS residual program undefined :- tnot(undefined). undefined.

If the toplevel_list_wfs_residual_program is false, any undefined answer is a conjunction with undefined/0. See the program and output below.

:- table p/0, q/0. p :- tnot(q). q :- tnot(p).

?- p. % WFS residual program p :- tnot(q). q :- tnot(p). p. ?- set_prolog_flag(toplevel_list_wfs_residual_program, false). true. ?- p. undefined.

Tag confusing pages with **doc-needs-help**|Tags are associated to your profile if you are logged in

Tags: