- tags
- Prolog
Notes
I Logic and Logic Programming
NOTER_PAGE: (15 . 0.2911676646706587)
1 A brief introduction to clausal logic
NOTER_PAGE: (17 . 0.312125748502994)
This reasoning pattern is called resolution
NOTER_PAGE: (20 . 0.6122754491017964)
NOTER_PAGE: (20 . 0.62874251497006)
in current logic programming systems the procedural interpretation does n o t exactly match the declarative interpretation
NOTER_PAGE: (20 . 0.7282934131736527)
NOTER_PAGE: (20 . 0.815868263473054)
the symbols ‘?-’ and ‘:-’ are in fact equivalent
NOTER_PAGE: (21 . 0.2784431137724551)
two definitions of a relation are (procedurally) equivalent if they have the same success set (restricted to that relation)
NOTER_PAGE: (21 . 0.46107784431137727)
recursion is the only looping structure
NOTER_PAGE: (22 . 0.17440119760479042)
what are the limits of expressiveness of clausal logic, i.e. what can and what cannot be expressed?
NOTER_PAGE: (29 . 0.44311377245508987)
what are the limits of reasoning with clausal logic, i.e. what can and what cannot be (efficiently) computed?
NOTER_PAGE: (29 . 0.47529940119760483)
2 Clausal logic and resolution: theoretical backgrounds
NOTER_PAGE: (31 . 0.3038922155688623)
answering queries is in fact no different from proving theorems
NOTER_PAGE: (31 . 0.5853293413173654)
Prolog is both unsound and incomplete. This has been a deliberate design choice: a sound and complete Prolog would be much less efficient.
NOTER_PAGE: (31 . 0.781437125748503)
programmer should know exactly the circumstances under which Prolog is unsound or incomplete, and avoid these circumstances in her programs.
NOTER_PAGE: (31 . 0.8091317365269461)
is it possible to detect these circumstances automatically, either in the reasoner or (better) in some kind of preprocessor?
definite clause logic, which is the subset of clausal logic used in Prolog
NOTER_PAGE: (32 . 0.22080838323353294)
relate clausal logic to Predicate Logic, and show that they are essentially equal in expressive power.
NOTER_PAGE: (32 . 0.2320359281437126)
2.1 Propositional clausal logic
NOTER_PAGE: (32 . 0.2911676646706587)
a proposition is any statement which is either true or false
NOTER_PAGE: (32 . 0.32335329341317365)
NOTER_PAGE: (32 . 0.33682634730538924)
Propositions are abstractly denoted by atoms, which are single words starting with a lowercase character
NOTER_PAGE: (32 . 0.37799401197604793)
NOTER_PAGE: (32 . 0.407185628742515)
The Herbrand base of a program P is the set of atoms occurring in P
NOTER_PAGE: (33 . 0.17664670658682635)
A Herbrand interpretation (or interpretation for short) for P is a mapping from the Herbrand base of P into the set of truth values {true, false}
NOTER_PAGE: (33 . 0.19236526946107785)
A Herbrand interpretation can be viewed as describing a possible state of affairs in the Universe of Discourse
NOTER_PAGE: (33 . 0.2350299401197605)
we could abbreviate such mappings by listing only the atoms that are assigned the truth value true
NOTER_PAGE: (33 . 0.2784431137724551)
the body of a clause is a conjunction of atoms, and the head is a disjunction
NOTER_PAGE: (33 . 0.3907185628742515)
statements like ‘if the moon is made of green cheese then 2 + 2 = 4’, in which there is no connection at all between body and head. One would like to say that such statements are neither true nor false. However, our semantics is not sophisticated enough to deal with this
NOTER_PAGE: (33 . 0.530688622754491)
married;bachelor:-man,adult can also be read as ‘someone is married or a bachelor or not a man or not an adult’. Thus, a clause is a disjunction of atoms, which are negated if they occur in the body of the clause
NOTER_PAGE: (33 . 0.6317365269461078)
If a clause is true in an interpretation, we say that the interpretation is a model for the clause. An interpretation is a model for a program if it is a model for each clause in the program.
NOTER_PAGE: (33 . 0.7455089820359282)
a clause C is a logical consequence of a program P if every model of the program is also a model of the clause; we write P C.
NOTER_PAGE: (34 . 0.2634730538922156)
in general, we only want to accept something as true if we are really forced to, i.e. if it is true in every possible model. This means that we should take the intersection of every model of a program in order to construct the intended model. In the example, this is {woman, human}. Note that this model is minimal in the sense that no subset of it is also a model. Therefore, this semantics is called a minimal model semantics.
NOTER_PAGE: (34 . 0.7118263473053893)
The program has in fact not one, but two minimal models, which is caused by the fact that the first clause has a disjunctive head. Such a clause is called indefinite
NOTER_PAGE: (35 . 0.2380239520958084)
if we would only allow definite clauses, i.e. clauses with a single positive literal, minimal models are guaranteed to be unique.
NOTER_PAGE: (35 . 0.2844311377245509)
Prolog is based on definite clause logic. In principle, this means that clauses like woman;man:-human are not expressible in Prolog
NOTER_PAGE: (35 . 0.31137724550898205)
The proof theory for clausal logic consists of a single inference rule called resolution.
NOTER_PAGE: (35 . 0.5815868263473054)
two clauses in the program are related to each other by means of the atom married, which occurs in the head of the first clause (a positive literal) and in the body of the second (a negative literal).
NOTER_PAGE: (36 . 0.38023952095808383)
the atom rectangle in the body of the first clause is replaced by the body of the second clause
NOTER_PAGE: (36 . 0.5800898203592815)
also referred to as unfolding
NOTER_PAGE: (36 . 0.594311377245509)
resolution is not complete at all!
NOTER_PAGE: (37 . 0.5014970059880239)
although resolution is unable to generate every logical consequence of a set of clauses, it is complete in the sense that resolution can always determine whether a specific clause is a logical consequence
NOTER_PAGE: (37 . 0.6309880239520959)
a is a logical consequence of P if, and only if, the empty clause can be deduced by resolution from P augmented with :-a.
NOTER_PAGE: (38 . 0.2470059880239521)
resolution is called refutation complete.
NOTER_PAGE: (38 . 0.27769461077844315)
maintain a list of previously derived clauses, and do not proceed with clauses that have been derived previously.
NOTER_PAGE: (38 . 0.5875748502994013)
this is not possible in the general case of full clausal logic, which is semi-decidable with respect to the question ‘is B a logical consequence of A’: there is an algorithm which derives, in finite time, a proof if one exists, but there is no algorithm which, for any A and B, halts and returns ‘no’ if no proof exists.
NOTER_PAGE: (38 . 0.6175149700598803)
2.2 Relational clausal logic
NOTER_PAGE: (39 . 0.17664670658682635)
NOTER_PAGE: (39 . 0.2986526946107785)
Individual names are called constants
NOTER_PAGE: (39 . 0.35853293413173654)
Arbitrary individuals are denoted by variables
NOTER_PAGE: (39 . 0.38323353293413176)
Jointly, constants and variables are denoted as terms. A ground term is a term without variables
NOTER_PAGE: (39 . 0.39895209580838326)
An atom is a predicate followed by a number of terms, enclosed in brackets and separated by commas, e.g. likes(peter,maria)
NOTER_PAGE: (39 . 0.4416167664670659)
The Herbrand universe of a program P is the set of ground terms (i.e. constants) occurring in it.
NOTER_PAGE: (39 . 0.7118263473053893)
The Herbrand base of P is the set of ground atoms that can be constructed using the predicates in P and the ground terms in the Herbrand universe. This set represents all the things we can say about the individuals in the Herbrand universe.
NOTER_PAGE: (39 . 0.7574850299401198)
It will sometimes be useful to rename the variables in clauses, such that no two clauses share a variable; this is called standardising the clauses apart.
NOTER_PAGE: (40 . 0.31886227544910184)
A substitution is a mapping from variables to terms. For example, {S!maria} and {S!X}
NOTER_PAGE: (40 . 0.5808383233532934)
A substitution can be applied to a clause
NOTER_PAGE: (40 . 0.594311377245509)
reasoning with ground clauses is just like reasoning with propositional clauses.
NOTER_PAGE: (40 . 0.7567365269461078)
An interpretation is a model for a non-ground clause if it is a model for every ground instance of the clause.
NOTER_PAGE: (40 . 0.7709580838323353)
Instead of applying arbitrary grounding substitutions before trying to apply resolution, we will derive the required substitutions from the clauses themselves.
NOTER_PAGE: (41 . 0.4633233532934132)
we do not require that exactly the same atom occurs in both clauses; rather, we require that there is a pair of atoms which can be made equal by substituting terms for variables.
NOTER_PAGE: (41 . 0.5172155688622755)
This process is called unification, and the substitution is called a unifier.
NOTER_PAGE: (41 . 0.690868263473054)
more general resolvents summarise a lot of less general ones. It therefore makes sense to derive only those resolvents that are as general as possible
NOTER_PAGE: (42 . 0.5673652694610779)
we are only interested in a most general unifier (mgu) of two literals
NOTER_PAGE: (42 . 0.5988023952095809)
As we have seen before, the actual proof method in clausal logic is proof by refutation. If we succeed in deriving the empty clause, then we have demonstrated that the set of clauses is inconsistent under the substitutions that are needed for unification of literals.
NOTER_PAGE: (42 . 0.6826347305389222)
Since the empty clause is derived, the query is indeed refuted, but only under the substitution {N!maria}, which constitutes the answer to the query.
NOTER_PAGE: (43 . 0.5576347305389222)
An important characteristic of relational clausal logic is that the Herbrand universe (the set of individuals we can reason about) is always finite
NOTER_PAGE: (44 . 0.2223053892215569)
relational clausal logic is decidable
NOTER_PAGE: (44 . 0.30538922155688625)
Full clausal logic allows us to reason about infinite domains by introducing more complex terms besides constants and variables
NOTER_PAGE: (44 . 0.6175149700598803)
We have given this person the abstract name person_loved_by(peter)
NOTER_PAGE: (44 . 0.7133233532934132)
Although there is no syntactic difference in full clausal logic between terms and atoms, their meaning and use is totally different
NOTER_PAGE: (45 . 0.3937125748502994)
A term always denotes an individual from the domain, while an atom denotes a proposition about individuals, which can get a truth value.
NOTER_PAGE: (45 . 0.42440119760479045)
the outcome of the mapping is a name, which is determined by unification.
NOTER_PAGE: (46 . 0.25224550898203596)
we introduce different names for individuals that might turn out to be identical
NOTER_PAGE: (46 . 0.312125748502994)
in the case of full clausal logic with infinite Herbrand universe you can go on applying resolution forever
NOTER_PAGE: (47 . 0.4528443113772455)
Resolution for full clausal logic is very similar to resolution for relational clausal logic: we only have to modify the unification algorithm in order to deal with complex terms.
NOTER_PAGE: (48 . 0.17664670658682635)
The disadvantage of the occur check is that it can be computationally very costly.
NOTER_PAGE: (49 . 0.35853293413173654)
decided to omit the occur check from Prolog’s unification algorithm. On the whole, this makes Prolog unsound; but this unsoundness only occurs in very specific cases, and it is the duty of the programmer to avoid such cases.
NOTER_PAGE: (49 . 0.4176646706586827)
we will show how an additional restriction on each of these variants will significantly improve the efficiency of a computational reasoning system for clausal logic. This is the restriction to definite clauses, on which Prolog is based.
NOTER_PAGE: (49 . 0.718562874251497)
definite clause logic is less expressive than full clausal logic, the main difference being that clausal logic can handle negative information.
NOTER_PAGE: (49 . 0.7627245508982037)
The way in which a clause is used in a resolution proof cannot be fixed in advance, because it depends on the thing we want to prove
NOTER_PAGE: (50 . 0.502994011976048)
this indeterminacy substantially increases the time it takes to find a refutation.
NOTER_PAGE: (50 . 0.5486526946107785)
solved by requiring that clauses have exactly one positive literal, which leads us into definite clause logic
NOTER_PAGE: (50 . 0.6339820359281437)
NOTER_PAGE: (51 . 0.3023952095808383)
If we want to extend definite clause logic to cover general clauses, we should extend resolution in order to deal with negated literals in the body of a clause.
NOTER_PAGE: (51 . 0.3323353293413174)
preferring a certain procedural interpretation corresponds to preferring a certain minimal model.
not can only be understood procedurally
NOTER_PAGE: (51 . 0.7881736526946108)
2.5 The relation between clausal logic and Predicate Logic
NOTER_PAGE: (52 . 0.17589820359281438)
NOTER_PAGE: (52 . 0.3226047904191617)
3 Logic Programming and Prolog
NOTER_PAGE: (57 . 0.3106287425149701)
In a purely declarative programming language, the programmer would have no means to express procedural knowledge, because logically equivalent programs would behave identical. However, Prolog is not a purely declarative language
NOTER_PAGE: (57 . 0.6601796407185629)
order of the literals in the body of a clause usually influences the efficiency of the program to a large degree.
NOTER_PAGE: (57 . 0.7035928143712575)
order of clauses in a program often determines whether a program will give an answer at all.
NOTER_PAGE: (57 . 0.7155688622754491)
3.1 SLD-resolution
NOTER_PAGE: (58 . 0.17514970059880242)
Prolog’s proof procedure is based on resolution refutation in definite clause logic.
NOTER_PAGE: (58 . 0.20883233532934134)
NOTER_PAGE: (58 . 0.23652694610778444)
Prolog’s selection rule is left to right
NOTER_PAGE: (58 . 0.49326347305389223)
This process is called SLD-resolution: S for selection rule, L for linear resolution (which refers to the shape of the proof trees obtained), and D for definite clauses.
NOTER_PAGE: (58 . 0.6062874251497007)
an SLD-tree may contain infinite branches, if some predicates in the program are recursive.
NOTER_PAGE: (59 . 0.43937125748503)
This is a rule of thumb that applies to most cases: put non-recursive clauses before recursive ones.
NOTER_PAGE: (60 . 0.5112275449101796)
Prolog will never discover that the query has in fact no answer, simply because the SLD-tree is infinite. So, one should be careful with programs like the above, which define a predicate to be symmetric.
NOTER_PAGE: (60 . 0.594311377245509)
we might never reach a success branch in the SLD-tree, because we get ‘trapped’ into an infinite subtree
NOTER_PAGE: (60 . 0.7799401197604791)
any infinite SLD-tree causes the inference engine to loop if no (more) answers are to be found.
NOTER_PAGE: (60 . 0.7926646706586827)
There exists a solution to this problem: if we descend the tree layer by layer rather than branch-by-branch, we will find any leaf before we descend to the next level. However, this also means that we must keep track of all the resolvents on a level, instead of just a single one. Therefore, this breadth-first search strategy needs much more memory
NOTER_PAGE: (61 . 0.23053892215568864)
Prolog’s incompleteness was a deliberate design choice, sacrifying completeness in order to obtain an efficient use of memory
NOTER_PAGE: (61 . 0.2881736526946108)
backtracking requires that all previous resolvents are remembered for which not all alternatives have been tried yet, together with a pointer to the most recent program clause that has been tried at that point.
NOTER_PAGE: (61 . 0.6324850299401198)
A node in the SLD-tree which is not a leaf is called a choice point
NOTER_PAGE: (62 . 0.49026946107784436)
how do we tell Prolog that a subtree contains only one success branch? For this, Prolog provides a control device which is called cut (written !)
NOTER_PAGE: (62 . 0.5785928143712575)
Note carefully that a cut does not prune every choice point. First of all, pruning does not occur above the choice point containing the head of the clause in which the cut is found. Secondly, choice points created by literals to the right of the cut, which are below the cut in the SLD-tree but are not yet on the stack when the cut is reached, are not pruned either
NOTER_PAGE: (63 . 0.5800898203592815)
If a cut prunes success branches, then some logical consequences of the program are not returned as answers, resulting in a procedural meaning different from the declarative meaning.
NOTER_PAGE: (63 . 0.6511976047904192)
the effect of a cut is not only determined by the clause in which it occurs but also by other clauses. Therefore, the effect of a cut is often hard to understand.
NOTER_PAGE: (64 . 0.8038922155688624)
Programs with cuts are not only difficult to understand; this last example also shows that their procedural interpretation (the set of answers they produce to a query) may be different from their declarative interpretation (the set of its logical consequences).
NOTER_PAGE: (65 . 0.46706586826347307)
incompatibility between declarative and procedural interpretation makes it a very problematic concept.
NOTER_PAGE: (66 . 0.17140718562874252)
higher- level constructs which have cleaner declarative meanings and which are easier to understand.
NOTER_PAGE: (66 . 0.19161676646706588)
3.3 Negation as failure
NOTER_PAGE: (66 . 0.44985029940119764)
very common use of cut: to ensure that the bodies of the clauses are mutually exclusive.
NOTER_PAGE: (67 . 0.25523952095808383)
built-in predicate call, which takes a goal as argument and succeeds if and only if execution of that goal succeeds.
NOTER_PAGE: (67 . 0.6541916167664671)
not(q) is proved by failing to prove q! Therefore, this kind of negation is called negation as failure.
NOTER_PAGE: (69 . 0.5374251497005988)
the program with not is slightly less efficient than the version with cut
NOTER_PAGE: (69 . 0.5666167664670659)
prefer the use of not, because it leads to programs of which the declarative meaning corresponds more closely to the procedural meaning.
NOTER_PAGE: (69 . 0.6639221556886228)
NOTER_PAGE: (71 . 0.35853293413173654)
if G is instantiated to a goal containing variables at the time not(G) is called, the result may be not in accordance with negation as failure. It is the programmer’s responsibility to avoid this. A simple remedy that will often work is to ensure the grounding of G by literals preceding not(G) in the body of the clause
NOTER_PAGE: (71 . 0.5838323353293413)
3.4 Other uses of cut
NOTER_PAGE: (72 . 0.3315868263473054)
his only works if the recursive call is the last call in the body. In general, it is advisable to write your recursive predicates like play above: the non-recursive clause before the recursive one, and the recursive call at the end of the body. A recursive predicate written this way is said to be tail recursive
NOTER_PAGE: (74 . 0.20733532934131738)
3.5 Arithmetic expressions
NOTER_PAGE: (74 . 0.33607784431137727)
multiplication as repeated addition is extremely inefficient compared to the algorithm for multiplicating numbers in decimal notation. Therefore, Prolog has built-in arithmetic facilities
NOTER_PAGE: (74 . 0.7664670658682635)
3.6 Accumulators
NOTER_PAGE: (77 . 0.17589820359281438)
NOTER_PAGE: (77 . 0.438622754491018)
since the accumulator is given an initial value of 0, it is always instantiated, such that the is literal can be placed before the recursive call.
NOTER_PAGE: (77 . 0.5883233532934132)
3.7 Second-order predicates
NOTER_PAGE: (80 . 0.36452095808383234)
generalise this program by including the relation which must hold
NOTER_PAGE: (80 . 0.5157185628742516)
Prolog provides access to its internal database where it stores the program clauses, by means of the built-in predicates assert and retract.
NOTER_PAGE: (81 . 0.23952095808383234)
NOTER_PAGE: (82 . 0.6706586826347306)
3.9 A methodology of Prolog programming
NOTER_PAGE: (88 . 0.5523952095808383)
II Reasoning with structured knowledge
NOTER_PAGE: (93 . 0.2881736526946108)
knowledge is structured if its components have certain logical relationships.
NOTER_PAGE: (93 . 0.561377245508982)
such structured knowledge has a convenient graphical representation
NOTER_PAGE: (93 . 0.6025449101796407)
d
such graphical structures are called graphs.
NOTER_PAGE: (93 . 0.6309880239520959)
the search space for the Towers of Hanoi grows exponentially with the number of disks. In practice, this means that the problem will be unsolvable for large n, no matter how efficient the search program
NOTER_PAGE: (95 . 0.7619760479041917)
Search is a problem solving method which, although applicable to almost any problem, has considerable practical limitations. Therefore, search is only applied to problems for which no analytic solutions are known.
NOTER_PAGE: (96 . 0.17514970059880242)
4 Representing structured knowledge
NOTER_PAGE: (97 . 0.3083832335329342)
when a path from n i to n j passes through a node which is also on a cycle, there are infinitely many different paths from n i to n j. Thus, a graph consisting of a limited number of nodes and arcs can generate infinite behaviour.
NOTER_PAGE: (97 . 0.562874251497006)
A tree is a special kind of graph which contains a root such that there is a unique path from the root to any other node.
NOTER_PAGE: (97 . 0.6175149700598803)
Only the most specific property regarding material is found, because of the cut in the recursive clause of properties/3.
NOTER_PAGE: (108 . 0.41092814371257486)
5 Searching graphs
NOTER_PAGE: (113 . 0.30763473053892215)
5.1 A general search procedure
NOTER_PAGE: (113 . 0.690868263473054)
Imagine a visit with a friend to the Staatsgalerie in Stuttgart
NOTER_PAGE: (113 . 0.722305389221557)
5.2 Depth-first search
NOTER_PAGE: (117 . 0.49251497005988026)
depth-first search is, in general, incomplete. Since Prolog itself employs depth-first search, Prolog is also incomplete. Often, however, the incompleteness of Prolog can be avoided by reordering the clauses
NOTER_PAGE: (119 . 0.22005988023952097)
depth- first search does not always find a shortest solution path.
NOTER_PAGE: (119 . 0.33458083832335334)
the size of the agenda is of the order B!"!n, that is, a linear function of the depth of the tree.
NOTER_PAGE: (119 . 0.43413173652694614)
If there is a chance that the search program gets trapped in an infinite loop, it might be a good idea to employ a predefined depth bound:
NOTER_PAGE: (119 . 0.659431137724551)
iterative deepening is complete
NOTER_PAGE: (120 . 0.3705089820359282)
A disadvantage of iterative deepening is that upper parts of the search space are searched more than once
NOTER_PAGE: (120 . 0.407934131736527)
5.3 Breadth-first search
NOTER_PAGE: (120 . 0.48428143712574856)
breadth-first search is complete, even for infinite search spaces
NOTER_PAGE: (121 . 0.17664670658682635)
d
breadth-first search always finds a shortest solution path.
NOTER_PAGE: (121 . 0.2065868263473054)
the number of nodes at depth n is B n , such that breadth-first search requires much more memory than depth-first search.
NOTER_PAGE: (121 . 0.23353293413173654)
5.4 Forward chaining
NOTER_PAGE: (124 . 0.5089820359281437)
NOTER_PAGE: (124 . 0.6100299401197605)
NOTER_PAGE: (131 . 0.30164670658682635)
NOTER_PAGE: (131 . 0.4356287425149701)
NOTER_PAGE: (131 . 0.4446107784431138)
6.1 Best-first search
NOTER_PAGE: (131 . 0.5913173652694611)
Recursive datastructures like lists are useful if the number of items to be stored is not fixed, but they require significantly more storage space.
NOTER_PAGE: (133 . 0.27619760479041916)
6.2 Optimal best-first search
NOTER_PAGE: (138 . 0.5411676646706587)
NOTER_PAGE: (141 . 0.17739520958083835)
Exhaustive search is often impractical, since the size of the agenda grows exponentially with the search depth. The use of a heuristic offers the possibility of keeping only a selection of best nodes on the agenda.
NOTER_PAGE: (141 . 0.23652694610778444)
III Advanced reasoning techniques
NOTER_PAGE: (144 . 0.29341317365269465)
NOTER_PAGE: (144 . 0.657185628742515)
increased expressiveness also requires more powerful semantics and proof theory.
NOTER_PAGE: (144 . 0.7709580838323353)
7 Reasoning with natural language
NOTER_PAGE: (147 . 0.30314371257485034)
NOTER_PAGE: (163 . 0.3106287425149701)
8.1 Default reasoning
NOTER_PAGE: (164 . 0.4910179640718563)
NOTER_PAGE: (166 . 0.7567365269461078)
distinguish between two possible types of rules, those with exceptions, and those without exceptions
NOTER_PAGE: (167 . 0.47455089820359286)
NOTER_PAGE: (170 . 0.2964071856287425)
NOTER_PAGE: (170 . 0.3278443113772455)
Closed World Assumption (CWA) states that everything that is not known to be true, must be false
NOTER_PAGE: (170 . 0.5127245508982037)
assumption that, in general, there are many more false statements that can be made than true statements
NOTER_PAGE: (170 . 0.5441616766467067)
hmmmm… what an interesting thought
NOTER_PAGE: (171 . 0.7956586826347306)
basic idea of Predicate Completion is to view each clause as part of the definition of a specific predicate
NOTER_PAGE: (172 . 0.18862275449101798)
definition can be completed by adding the only-if parts, resulting in a full definition: ‘X likes Y if and only if …’. Such a full definition is most easily expressed in Predicate Logic.
NOTER_PAGE: (172 . 0.27395209580838326)
in this case, Comp(P) and CWA(P) are logically equivalent. This is true in general, provided P is a set of definite clauses. Predicate Completion extends the Closed World Assumption by also being able to handle programs containing general clauses
NOTER_PAGE: (173 . 0.7327844311377246)
8.3 Abduction and diagnostic reasoning
NOTER_PAGE: (175 . 0.17814371257485032)
Abduction extends default reasoning by not only making assumptions about what is false, but also about what is true.
NOTER_PAGE: (175 . 0.20733532934131738)
abductive explanations are usually restricted to ground literals with predicates that are undefined in Theory (such literals are called abducibles)
NOTER_PAGE: (175 . 0.4633233532934132)
Procedurally, we can construct an abductive explanation by trying to prove the Observation from the initial Theory alone: whenever we encounter a literal for which there is no clause to resolve with, we add the literal to the Explanation.
NOTER_PAGE: (175 . 0.5217065868263473)
we have to deal explicitly with negated literals in our abduction program
NOTER_PAGE: (176 . 0.6609281437125749)
this approach relies on the fact that negated literals are checked after the abductive explanation has been constructed
NOTER_PAGE: (177 . 0.3315868263473054)
8.4 The complete picture
NOTER_PAGE: (182 . 0.3847305389221557)
9 Inductive reasoning
NOTER_PAGE: (187 . 0.30538922155688625)
NOTER_PAGE: (187 . 0.4139221556886228)
A A catalogue of useful predicates
NOTER_PAGE: (211 . 0.31736526946107785)
C Answers to selected exercises
NOTER_PAGE: (227 . 0.31736526946107785)