/
PLFCEntails.java
199 lines (184 loc) · 7.18 KB
/
PLFCEntails.java
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
package aima.core.logic.propositional.inference;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import aima.core.logic.propositional.kb.KnowledgeBase;
import aima.core.logic.propositional.kb.data.Clause;
import aima.core.logic.propositional.parsing.ast.PropositionSymbol;
import aima.core.logic.propositional.transformations.ConvertToConjunctionOfClauses;
import aima.core.logic.propositional.transformations.SymbolCollector;
/**
* Artificial Intelligence A Modern Approach (3rd Edition): page 258.<br>
* <br>
*
* <pre>
* <code>
* function PL-FC-ENTAILS?(KB, q) returns true or false
* inputs: KB, the knowledge base, a set of propositional definite clauses
* q, the query, a proposition symbol
* count ← a table, where count[c] is the number of symbols in c's premise
* inferred ← a table, where inferred[s] is initially false for all symbols
* agenda ← a queue of symbols, initially symbols known to be true in KB
*
* while agenda is not empty do
* p ← Pop(agenda)
* if p = q then return true
* if inferred[p] = false then
* inferred[p] ← true
* for each clause c in KB where p is in c.PREMISE do
* decrement count[c]
* if count[c] = 0 then add c.CONCLUSION to agenda
* return false
* </code>
* </pre>
*
* Figure 7.15 the forward-chaining algorithm for propositional logic. The
* <i>agenda</i> keeps track of symbols known to be true but not yet
* "processed". The <i>count</i> table keeps track of how many premises of each
* implication are as yet unknown. Whenever a new symbol p from the agenda is
* processed, the count is reduced by one for each implication in whose premise
* p appears (easily identified in constant time with appropriate indexing.) If
* a count reaches zero, all the premises of the implication are known, so its
* conclusion can be added to the agenda. Finally, we need to keep track of
* which symbols have been processed; a symbol that is already in the set of
* inferred symbols need not be added to the agenda again. This avoids redundant
* work and prevents loops caused by implications such as P ⇒ Q and Q
* ⇒ P.
*
* @author Ciaran O'Reilly
* @author Ravi Mohan
* @author Mike Stampone
*/
public class PLFCEntails {
/**
* PL-FC-ENTAILS?(KB, q)<br>
* The forward-chaining algorithm for propositional logic.
*
* @param kb
* the knowledge base, a set of propositional definite clauses.
* @param q
* q, the query, a proposition symbol
* @return true if KB |= q, false otherwise.
* @throws IllegalArgumentException
* if KB contains any non-definite clauses.
*/
public boolean isEntailed(KnowledgeBase kb, PropositionSymbol q) {
// count <- a table, where count[c] is the number of symbols in c's
// premise
Map<Clause, Integer> count = initializeCount(kb);
// inferred <- a table, where inferred[s] is initially false for all
// symbols
Map<PropositionSymbol, Boolean> inferred = initializeInferred(kb);
// agenda <- a queue of symbols, initially symbols known to be true in
// KB
Queue<PropositionSymbol> agenda = initializeAgenda(count);
// Note: an index for p to the clauses where p appears in the premise
Map<PropositionSymbol, Set<Clause>> pToClausesWithPInPremise = initializeIndex(
count, inferred);
// while agenda is not empty do
while (!agenda.isEmpty()) {
// p <- Pop(agenda)
PropositionSymbol p = agenda.remove();
// if p = q then return true
if (p.equals(q)) {
return true;
}
// if inferred[p] = false then
if (inferred.get(p).equals(Boolean.FALSE)) {
// inferred[p] <- true
inferred.put(p, true);
// for each clause c in KB where p is in c.PREMISE do
for (Clause c : pToClausesWithPInPremise.get(p)) {
// decrement count[c]
decrement(count, c);
// if count[c] = 0 then add c.CONCLUSION to agenda
if (count.get(c) == 0) {
agenda.add(conclusion(c));
}
}
}
}
// return false
return false;
}
//
// SUPPORTING CODE
//
//
// PROTECTED
//
protected Map<Clause, Integer> initializeCount(KnowledgeBase kb) {
// count <- a table, where count[c] is the number of symbols in c's
// premise
Map<Clause, Integer> count = new HashMap<Clause, Integer>();
Set<Clause> clauses = ConvertToConjunctionOfClauses.apply(
kb.asSentence()).getClauses();
for (Clause c : clauses) {
if (!c.isDefiniteClause()) {
throw new IllegalArgumentException(
"Knowledge Base contains non-definite clauses:" + c);
}
// Note: # of negative literals is equivalent to the number of
// symbols in c's premise
count.put(c, c.getNumberNegativeLiterals());
}
return count;
}
protected Map<PropositionSymbol, Boolean> initializeInferred(KnowledgeBase kb) {
// inferred <- a table, where inferred[s] is initially false for all
// symbols
Map<PropositionSymbol, Boolean> inferred = new HashMap<PropositionSymbol, Boolean>();
for (PropositionSymbol p : SymbolCollector.getSymbolsFrom(kb
.asSentence())) {
inferred.put(p, false);
}
return inferred;
}
// Note: at the point of calling this routine, count will contain all the
// clauses in KB.
protected Queue<PropositionSymbol> initializeAgenda(Map<Clause, Integer> count) {
// agenda <- a queue of symbols, initially symbols known to be true in
// KB
Queue<PropositionSymbol> agenda = new LinkedList<PropositionSymbol>();
for (Clause c : count.keySet()) {
// No premise just a conclusion, then we know its true
if (c.getNumberNegativeLiterals() == 0) {
agenda.add(conclusion(c));
}
}
return agenda;
}
// Note: at the point of calling this routine, count will contain all the
// clauses in KB while inferred will contain all the proposition symbols.
protected Map<PropositionSymbol, Set<Clause>> initializeIndex(
Map<Clause, Integer> count, Map<PropositionSymbol, Boolean> inferred) {
Map<PropositionSymbol, Set<Clause>> pToClausesWithPInPremise = new HashMap<PropositionSymbol, Set<Clause>>();
for (PropositionSymbol p : inferred.keySet()) {
Set<Clause> clausesWithPInPremise = new HashSet<Clause>();
for (Clause c : count.keySet()) {
// Note: The negative symbols comprise the premise
if (c.getNegativeSymbols().contains(p)) {
clausesWithPInPremise.add(c);
}
}
pToClausesWithPInPremise.put(p, clausesWithPInPremise);
}
return pToClausesWithPInPremise;
}
protected void decrement(Map<Clause, Integer> count, Clause c) {
int currentCount = count.get(c);
// Note: a definite clause can just be a fact (i.e. 1 positive literal)
// However, we only decrement those where the symbol is in the premise
// so we don't need to worry about going < 0.
count.put(c, currentCount - 1);
}
protected PropositionSymbol conclusion(Clause c) {
// Note: the conclusion is from the single positive
// literal in the definite clause (which we are
// restricted to).
return c.getPositiveSymbols().iterator().next();
}
}