| Interface | Description |
|---|---|
| InferenceProcedure | |
| InferenceResult |
| Class | Description |
|---|---|
| AbstractModulation |
Abstract base class for Demodulation and Paramodulation algorithms.
|
| Demodulation |
Artificial Intelligence A Modern Approach (3rd Edition): page 354.
Demodulation: For any terms x, y, and z, where z appears somewhere in literal mi and where UNIFY(x,z) = θ: |
| FOLBCAsk |
Artificial Intelligence A Modern Approach (2nd Edition): Figure 9.6, page
288.
|
| FOLFCAsk |
Artificial Intelligence A Modern Approach (3rd Edition): Figure 9.3, page
332.
|
| FOLModelElimination |
Based on lecture notes from:
http://logic.stanford.edu/classes/cs157/2008/lectures/lecture13.pdf |
| FOLOTTERLikeTheoremProver |
Artificial Intelligence A Modern Approach (2nd Edition): Figure 9.14, page
307.
|
| FOLTFMResolution |
Artificial Intelligence A Modern Approach (3rd Edition): page 347.
The algorithmic approach is identical to the propositional case, described in Figure 7.12. However, this implementation will use the T)wo F)inger M)ethod for looking for resolvents between clauses, which is very inefficient. see: http://logic.stanford.edu/classes/cs157/2008/lectures/lecture04.pdf, slide 21 for the propositional case. |
| InferenceResultPrinter | |
| Paramodulation |
Artificial Intelligence A Modern Approach (3r Edition): page 354.
Paramodulation: For any terms x, y, and z, where z appears somewhere in literal mi, and where UNIFY(x,z) = θ, |