Skip to content

Commit

Permalink
Merge branch 'master' of https://github.com/naveensundarg/prover
Browse files Browse the repository at this point in the history 
# Conflicts:
#	src/main/java/com/naveensundarg/shadow/prover/core/proof/AtomicJustification.java
  • Loading branch information
@naveensundarg
naveensundarg committed Aug 18, 2018
2 parents cae22c6 + 64041ec commit d6ba307
Show file tree
Hide file tree
Showing 14 changed files with 514 additions and 78 deletions.
60 changes: 28 additions & 32 deletions pom.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@

<groupId>com.naveensundarg</groupId>
<artifactId>prover</artifactId>
<version>0.998</version>
<version>1.02</version>
<packaging>jar</packaging>


Expand All @@ -31,38 +31,34 @@
<tag>HEAD</tag>
</scm>

<distributionManagement>
<snapshotRepository>
<id>ossrh</id>
<url>https://oss.sonatype.org/content/repositories/snapshots</url>
</snapshotRepository>
<repository>
<id>ossrh</id>
<url>https://oss.sonatype.org/service/local/staging/deploy/maven2/</url>
</repository>
</distributionManagement>

<build>
<pluginManagement>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-gpg-plugin</artifactId>
<version>1.5</version>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-release-plugin</artifactId>
<configuration>
<checkModificationExcludes>
<checkModificationExclude>pom.xml</checkModificationExclude>
</checkModificationExcludes>
</configuration>
<version>2.4</version>
</plugin>


</plugins>
</pluginManagement>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-assembly-plugin</artifactId>
<version>2.2-beta-5</version>
<configuration>
<descriptorRefs>
<descriptorRef>jar-with-dependencies</descriptorRef>
</descriptorRefs>
<archive>
<manifest>
<mainClass>com.naveensundarg.shadow.prover.sandboxes.Sandbox</mainClass>
</manifest>
</archive>
</configuration>
<executions>
<execution>
<id>make-assembly</id>
<phase>package</phase>
<goals>
<goal>single</goal>
</goals>
</execution>
</executions>
</plugin>
</plugins>
</build>


Expand Down
11 changes: 5 additions & 6 deletions snark-20120808r02/snark-interface.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@
(assert `(= ,(+ i j) (+ ,j ,i ))))))

(defun assert-domain (end)
(assert `(forall ((?p Number))
(assert `(forall (?p)
(implies (Prior ?p ,end)
,(cons 'or (loop for i from 0 to end collect
`(= ,i ?p)))))))
Expand All @@ -56,10 +56,10 @@



(defun setup-snark (&key (time-limit 500) (verbose t))
(defun setup-snark (&key (time-limit 500) (verbose nil))

(snark:initialize :verbose verbose)
;(if (not verbose) (snark-deverbose) )
(if (not verbose) (snark-deverbose) )
(snark:run-time-limit time-limit)
(snark:assert-supported t)
(snark:assume-supported t)
Expand All @@ -69,9 +69,8 @@
(snark::declare-code-for-numbers)

(snark:allow-skolem-symbols-in-answers nil)
;(assert-domain 10)
;(assert-add-table 10)
)
(assert-domain 10)
(assert-add-table 10))



Expand Down
78 changes: 55 additions & 23 deletions src/main/java/com/naveensundarg/shadow/prover/core/ccprovers/CognitiveCalculusProver.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
import com.diogonunes.jcdp.color.ColoredPrinter;
import com.diogonunes.jcdp.color.api.Ansi;
import com.naveensundarg.shadow.prover.core.Logic;
import com.naveensundarg.shadow.prover.core.proof.AtomicJustification;
import com.naveensundarg.shadow.prover.utils.*;
import com.naveensundarg.shadow.prover.core.Prover;
import com.naveensundarg.shadow.prover.core.SnarkWrapper;
Expand Down Expand Up @@ -138,6 +139,13 @@ private static CognitiveCalculusProver root(CognitiveCalculusProver cognitiveCal
@Override
public Optional<Justification> prove(Set<Formula> assumptions, Formula formula) {

assumptions.forEach(x-> {

if(x.getJustification() == null){

x.setJustification(new AtomicJustification("GIVEN"));
}
});
return prove(assumptions, formula, CollectionUtils.newEmptySet());
}

Expand Down Expand Up @@ -169,19 +177,7 @@ private boolean alreadySeen(Set<Formula> assumptions, Formula formula) {
private synchronized Optional<Justification> prove(Set<Formula> assumptions, Formula formula, Set<Formula> added) {


currentAssumptions = assumptions;


if (defeasible) {

Optional<Justification> got = defeasible(formula);

if (got != null) return got;

} else {


}


Prover folProver = SnarkWrapper.getInstance();
Expand All @@ -204,7 +200,7 @@ private synchronized Optional<Justification> prove(Set<Formula> assumptions, For
int sizeAfterExpansion = base.size();

if (base.contains(formula)) {
return Optional.of(TrivialJustification.trivial(assumptions, formula));
return Optional.of(TrivialJustification.trivial(base, formula));
}

Optional<Justification> andProofOpt = tryAND(base, formula, added);
Expand Down Expand Up @@ -288,17 +284,10 @@ private synchronized Optional<Justification> prove(Set<Formula> assumptions, For
// logFOLCall(true, shadow(base), shadowedGoal);
return shadowedJustificationOpt;
}
else{

// logFOLCall(false, shadow(base), shadowedGoal);
// logFOLCall(false, shadow(base), shadowedGoal);

}
if (agentClosureJustificationOpt.isPresent()) {

return agentClosureJustificationOpt;
}
return agentClosureJustificationOpt;

return Optional.empty();
}

protected Optional<Justification> tryIfIntro(Set<Formula> base, Formula formula, Set<Formula> added) {
Expand Down Expand Up @@ -729,6 +718,9 @@ protected Set<Formula> expand(Set<Formula> base, Set<Formula> added, Formula goa
expandR4(base, added);
expandSelfBelief(base, added);
expandPerceptionToKnowledge(base, added);
expandSaysToBelief(base, added);
expandIntentionToPerception(base, added);

expandModalConjunctions(base, added);
expandModalImplications(base, added);
expandDR1(base, added, goal);
Expand Down Expand Up @@ -885,12 +877,52 @@ private void expandPerceptionToKnowledge(Set<Formula> base, Set<Formula> added)
filter(f -> f instanceof Perception).
map(f -> {
Perception p = (Perception) f;
return new Knowledge(p.getAgent(), p.getTime(), p.getFormula());
Knowledge k = new Knowledge(p.getAgent(), p.getTime(), p.getFormula());
k.setJustification(new CompoundJustification("Perception to knowledge " + p, CollectionUtils.listOf(p.getJustification())));
return k;
}).
collect(Collectors.toSet());

expansionLog(String.format("Perceives(P) ==> P", Constants.VDASH, Constants.PHI, Constants.NEC, Constants.PHI), derived);

base.addAll(derived);
added.addAll(derived);
}

private void expandIntentionToPerception(Set<Formula> base, Set<Formula> added) {

Set<Formula> derived = base.
stream().
filter(f -> f instanceof Intends).
map(f -> {
Intends i = (Intends) f;
Perception k = new Perception(i.getAgent(), i.getTime(), i.getFormula());
k.setJustification(new CompoundJustification("Intention to Perception " + i, CollectionUtils.listOf(i.getJustification())));
return k;
}).
collect(Collectors.toSet());

expansionLog(String.format("Intends(P) ==> Perceives(P)", Constants.VDASH, Constants.PHI, Constants.NEC, Constants.PHI), derived);

base.addAll(derived);
added.addAll(derived);
}

private void expandSaysToBelief(Set<Formula> base, Set<Formula> added) {

Set<Formula> derived = base.
stream().
filter(f -> f instanceof Says).
map(f -> {
Says s = (Says) f;
Belief b = new Belief(s.getAgent(), s.getTime(), s.getFormula());
b.setJustification(new CompoundJustification("Says to belief", CollectionUtils.listOf(s.getJustification())));
return b;
}).
collect(Collectors.toSet());

expansionLog(String.format("Says(P) ==> Belief(P)", Constants.VDASH, Constants.PHI, Constants.NEC, Constants.PHI), derived);

base.addAll(derived);
added.addAll(derived);

Expand Down
Loading

0 comments on commit d6ba307

Please sign in to comment.