Skip to content

Commit a110ece

Browse files
ShobhitLambaShobhitLamba
committed
Modulation algorithms added to logic
1 parent 27cc38f commit a110ece

File tree

4 files changed

+648
-0
lines changed

4 files changed

+648
-0
lines changed

‎aima-csharp/aima-csharp.csproj‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,7 @@
107107
<Compile Include="logic\common\ParserException.cs" />
108108
<Compile Include="logic\common\ParserTreeNode.cs" />
109109
<Compile Include="logic\common\Token.cs" />
110+
<Compile Include="logic\fol\CNFConverter.cs" />
110111
<Compile Include="logic\fol\Connectors.cs" />
111112
<Compile Include="logic\fol\domain\DomainFactory.cs" />
112113
<Compile Include="logic\fol\domain\FOLDomain.cs" />
@@ -115,6 +116,8 @@
115116
<Compile Include="logic\fol\domain\FOLDomainListener.cs" />
116117
<Compile Include="logic\fol\domain\FOLDomainSkolemConstantAddedEvent.cs" />
117118
<Compile Include="logic\fol\domain\FOLDomainSkolemFunctionAddedEvent.cs" />
119+
<Compile Include="logic\fol\inference\AbstractModulation.cs" />
120+
<Compile Include="logic\fol\inference\Demodulation.cs" />
118121
<Compile Include="logic\fol\inference\InferenceProcedure.cs" />
119122
<Compile Include="logic\fol\inference\InferenceResult.cs" />
120123
<Compile Include="logic\fol\inference\InferenceResultPrinter.cs" />
@@ -124,6 +127,7 @@
124127
<Compile Include="logic\fol\inference\otter\defaultimpl\DefaultClauseSimplifier.cs" />
125128
<Compile Include="logic\fol\inference\otter\defaultimpl\DefaultLightestClauseHeuristic.cs" />
126129
<Compile Include="logic\fol\inference\otter\LightestClauseHeuristic.cs" />
130+
<Compile Include="logic\fol\inference\Paramodulation.cs" />
127131
<Compile Include="logic\fol\inference\proof\AbstractProofStep.cs" />
128132
<Compile Include="logic\fol\inference\proof\Proof.cs" />
129133
<Compile Include="logic\fol\inference\proof\ProofFinal.cs" />
@@ -170,7 +174,15 @@
170174
<Compile Include="logic\fol\parsing\FOLLexer.cs" />
171175
<Compile Include="logic\fol\parsing\FOLParser.cs" />
172176
<Compile Include="logic\fol\parsing\FOLVisitor.cs" />
177+
<Compile Include="logic\fol\PredicateCollector.cs" />
173178
<Compile Include="logic\fol\Quantifiers.cs" />
179+
<Compile Include="logic\fol\StandardizeApart.cs" />
180+
<Compile Include="logic\fol\StandardizeApartIndexical.cs" />
181+
<Compile Include="logic\fol\StandardizeApartIndexicalFactory.cs" />
182+
<Compile Include="logic\fol\StandardizeApartInPlace.cs" />
183+
<Compile Include="logic\fol\StandardizeApartResult.cs" />
184+
<Compile Include="logic\fol\SubstVisitor.cs" />
185+
<Compile Include="logic\fol\SubsumptionElimination.cs" />
174186
<Compile Include="logic\fol\Unifier.cs" />
175187
<Compile Include="logic\fol\VariableCollector.cs" />
176188
<Compile Include="obj\Debug\TemporaryGeneratedFile_036C0B5B-1481-4323-8D20-8F5ADCB23D92.cs" />

‎aima-csharp/logic/fol/inference/AbstractModulation.cs‎

Lines changed: 288 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,288 @@
1+
using System;
2+
using System.Collections.Generic;
3+
using aima.core.logic.fol;
4+
using aima.core.logic.fol.parsing;
5+
using aima.core.logic.fol.parsing.ast;
6+
7+
namespace aima.core.logic.fol.inference
8+
{
9+
/**
10+
* Abstract base class for Demodulation and Paramodulation algorithms.
11+
*
12+
* @author Ciaran O'Reilly
13+
*
14+
*/
15+
public abstract class AbstractModulation
16+
{
17+
// PROTECTED ATTRIBUTES
18+
protected VariableCollector variableCollector = new VariableCollector();
19+
protected Unifier unifier = new Unifier();
20+
protected SubstVisitor substVisitor = new SubstVisitor();
21+
22+
// PROTECTED METODS
23+
public abstract bool isValidMatch(Term toMatch,
24+
List<Variable> toMatchVariables, Term possibleMatch,
25+
Dictionary<Variable, Term> substitution);
26+
27+
protected IdentifyCandidateMatchingTerm getMatchingSubstitution(
28+
Term toMatch, AtomicSentence expression)
29+
{
30+
31+
IdentifyCandidateMatchingTerm icm = new IdentifyCandidateMatchingTerm(
32+
toMatch, expression, this);
33+
34+
if (icm.isMatch())
35+
{
36+
return icm;
37+
}
38+
// indicates no match
39+
return null;
40+
}
41+
42+
protected class IdentifyCandidateMatchingTerm : FOLVisitor
43+
{
44+
private Term toMatch = null;
45+
private List<Variable> toMatchVariables = null;
46+
private Term matchingTerm = null;
47+
private Dictionary<Variable, Term> substitution = null;
48+
private AbstractModulation abstractModulation;
49+
50+
public IdentifyCandidateMatchingTerm(Term toMatch,
51+
AtomicSentence expression, AbstractModulation abstractModulation)
52+
{
53+
this.abstractModulation = abstractModulation;
54+
this.toMatch = toMatch;
55+
this.toMatchVariables = abstractModulation.variableCollector
56+
.collectAllVariables(toMatch);
57+
58+
expression.accept(this, null);
59+
}
60+
61+
public bool isMatch()
62+
{
63+
return null != matchingTerm;
64+
}
65+
66+
public Term getMatchingTerm()
67+
{
68+
return matchingTerm;
69+
}
70+
71+
public Dictionary<Variable, Term> getMatchingSubstitution()
72+
{
73+
return substitution;
74+
}
75+
76+
// START-FOLVisitor
77+
public Object visitPredicate(Predicate p, Object arg)
78+
{
79+
foreach (Term t in p.getArgs())
80+
{
81+
// Finish processing if have found a match
82+
if (null != matchingTerm)
83+
{
84+
break;
85+
}
86+
t.accept(this, null);
87+
}
88+
return p;
89+
}
90+
91+
public Object visitTermEquality(TermEquality equality, Object arg)
92+
{
93+
foreach (Term t in equality.getArgs())
94+
{
95+
// Finish processing if have found a match
96+
if (null != matchingTerm)
97+
{
98+
break;
99+
}
100+
t.accept(this, null);
101+
}
102+
return equality;
103+
}
104+
105+
public Object visitVariable(Variable variable, Object arg)
106+
{
107+
108+
if (null != (substitution = abstractModulation.unifier.unify(toMatch, variable)))
109+
{
110+
if (abstractModulation.isValidMatch(toMatch, toMatchVariables, variable,
111+
substitution))
112+
{
113+
matchingTerm = variable;
114+
}
115+
}
116+
return variable;
117+
}
118+
119+
public Object visitConstant(Constant constant, Object arg)
120+
{
121+
if (null != (substitution = abstractModulation.unifier.unify(toMatch, constant)))
122+
{
123+
if (abstractModulation.isValidMatch(toMatch, toMatchVariables, constant,
124+
substitution))
125+
{
126+
matchingTerm = constant;
127+
}
128+
}
129+
return constant;
130+
}
131+
132+
public Object visitFunction(Function function, Object arg)
133+
{
134+
if (null != (substitution = abstractModulation.unifier.unify(toMatch, function)))
135+
{
136+
if (abstractModulation.isValidMatch(toMatch, toMatchVariables, function,
137+
substitution))
138+
{
139+
matchingTerm = function;
140+
}
141+
}
142+
143+
if (null == matchingTerm)
144+
{
145+
// Try the Function's arguments
146+
foreach (Term t in function.getArgs())
147+
{
148+
// Finish processing if have found a match
149+
if (null != matchingTerm)
150+
{
151+
break;
152+
}
153+
t.accept(this, null);
154+
}
155+
}
156+
return function;
157+
}
158+
159+
public Object visitNotSentence(NotSentence sentence, Object arg)
160+
{
161+
throw new NotImplementedException(
162+
"visitNotSentence() should not be called.");
163+
}
164+
165+
public Object visitConnectedSentence(ConnectedSentence sentence,
166+
Object arg)
167+
{
168+
throw new NotImplementedException(
169+
"visitConnectedSentence() should not be called.");
170+
}
171+
172+
public Object visitQuantifiedSentence(QuantifiedSentence sentence,
173+
Object arg)
174+
{
175+
throw new NotImplementedException(
176+
"visitQuantifiedSentence() should not be called.");
177+
}
178+
// END-FOLVisitor
179+
}
180+
181+
protected class ReplaceMatchingTerm : FOLVisitor
182+
{
183+
private Term toReplace = null;
184+
private Term replaceWith = null;
185+
private bool replaced = false;
186+
187+
public ReplaceMatchingTerm()
188+
{
189+
}
190+
191+
public AtomicSentence replace(AtomicSentence expression,
192+
Term toReplace, Term replaceWith)
193+
{
194+
this.toReplace = toReplace;
195+
this.replaceWith = replaceWith;
196+
197+
return (AtomicSentence)expression.accept(this, null);
198+
}
199+
200+
//
201+
// START-FOLVisitor
202+
public Object visitPredicate(Predicate p, Object arg)
203+
{
204+
List<Term> newTerms = new List<Term>();
205+
foreach (Term t in p.getTerms())
206+
{
207+
Term subsTerm = (Term)t.accept(this, arg);
208+
newTerms.Add(subsTerm);
209+
}
210+
return new Predicate(p.getPredicateName(), newTerms);
211+
}
212+
213+
public Object visitTermEquality(TermEquality equality, Object arg)
214+
{
215+
Term newTerm1 = (Term)equality.getTerm1().accept(this, arg);
216+
Term newTerm2 = (Term)equality.getTerm2().accept(this, arg);
217+
return new TermEquality(newTerm1, newTerm2);
218+
}
219+
220+
public Object visitVariable(Variable variable, Object arg)
221+
{
222+
if (!replaced)
223+
{
224+
if (toReplace.Equals(variable))
225+
{
226+
replaced = true;
227+
return replaceWith;
228+
}
229+
}
230+
return variable;
231+
}
232+
233+
public Object visitConstant(Constant constant, Object arg)
234+
{
235+
if (!replaced)
236+
{
237+
if (toReplace.Equals(constant))
238+
{
239+
replaced = true;
240+
return replaceWith;
241+
}
242+
}
243+
return constant;
244+
}
245+
246+
public Object visitFunction(Function function, Object arg)
247+
{
248+
if (!replaced)
249+
{
250+
if (toReplace.Equals(function))
251+
{
252+
replaced = true;
253+
return replaceWith;
254+
}
255+
}
256+
257+
List<Term> newTerms = new List<Term>();
258+
foreach (Term t in function.getTerms())
259+
{
260+
Term subsTerm = (Term)t.accept(this, arg);
261+
newTerms.Add(subsTerm);
262+
}
263+
return new Function(function.getFunctionName(), newTerms);
264+
}
265+
266+
public Object visitNotSentence(NotSentence sentence, Object arg)
267+
{
268+
throw new NotImplementedException(
269+
"visitNotSentence() should not be called.");
270+
}
271+
272+
public Object visitConnectedSentence(ConnectedSentence sentence,
273+
Object arg)
274+
{
275+
throw new NotImplementedException(
276+
"visitConnectedSentence() should not be called.");
277+
}
278+
279+
public Object visitQuantifiedSentence(QuantifiedSentence sentence,
280+
Object arg)
281+
{
282+
throw new NotImplementedException(
283+
"visitQuantifiedSentence() should not be called.");
284+
}
285+
// END-FOLVisitor
286+
}
287+
}
288+
}

0 commit comments

Comments
 (0)