Skip to content
This repository has been archived by the owner on Oct 11, 2023. It is now read-only.
/ prover Public archive
forked from naveensundarg/prover

This fork of ShadowProver is used as a submodule by ShadowAdjudicator and should not be moved.

Notifications You must be signed in to change notification settings

RAIRLab/prover

 
 

Repository files navigation

ShadowProver

ShadowProver is a theorem prover (multi-modal logic with quantifiers).

There is a Python API for the prover. (Requires docker to run the prover in a clean container.)

To start the prover

cd prover
docker-compose up
from interface import prove

assumptions = [
    "(Believes! john happy)", 
    "(Believes! john smiling)" ]

goal = "(Believes! john (and happy smiling))"

prove(assumptions, goal)

Under the hood

ShadowProver is a novel multi-modal + extensional logic theorem prover that uses a technique called shadowing to achieve speed without sacrificing consistency in the system. Extant first-order modal logic theorem provers that can work with arbitrary inference schemata are built upon first-order theorem provers. They achieve the reduction to first-order logic via two methods. In the first method, modal operators are simply represented by first-order predicates. This approach is the fastest but can quickly lead to well-known inconsistencies as demonstrated in [Bringsjord and Govindarajulu, 2012] (see the Slate proof below). In the second method, the entire proof theory is implemented intricately in first-order logic, and the reasoning is carried out within first-order logic. Here, the first-order theorem prover simply functions as a declarative programming system. This approach, while accurate, can be excruciatingly slow.

We use a different approach, in which we alternate between calling a first-order theorem prover and applying modal inference schemata. When we call the first-order prover, all modal atoms are converted into propositional atoms (i.e., shadowing), to prevent substitution into modal contexts. This approach achieves speed without sacrificing consistency. The prover also lets us add arbitrary inference schemata to the calculus by using a special-purpose language. While we use the prover in our simulations, describing the prover in more detail is out of scope for the present paper.

References

[Bringsjord and Govindarajulu, 2012] Selmer Bringsjord and Naveen Sundar Govindarajulu. Given the Web, What is Intelligence, Really? Metaphilosophy, 43(4):361–532, 2012.

Resources

For more details see:

https://drive.google.com/open?id=0B9Vb2O21ibhaZTNLd21wd21adjg

About

This fork of ShadowProver is used as a submodule by ShadowAdjudicator and should not be moved.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Common Lisp 50.2%
  • Java 27.2%
  • Clojure 12.4%
  • HTML 9.6%
  • Jupyter Notebook 0.2%
  • CSS 0.2%
  • Other 0.2%