Skip to content

Instantly share code, notes, and snippets.

@naveensundarg

naveensundarg/Self-Sacrifice.md Secret

Forked from IJCAI2017-3841/Code.md
Last active July 21, 2017 08:17
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save naveensundarg/c01d956ddb9a0caf5f3ca0e0b40a1506 to your computer and use it in GitHub Desktop.
Save naveensundarg/c01d956ddb9a0caf5f3ca0e0b40a1506 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Self-Sacrifice.md

Prerequisites

  1. Common Lisp (tested on SBCL [http://sbcl.org] & ABCL [https://common-lisp.net/project/armedbear ])
  2. Java 8 (or above)
  3. SRI's SNARK ATP: http://www.ai.sri.com/~stickel/snark.html
  4. Build tools: Maven

The prover is a combination of Java and Common Lisp code (loaded into Java using ABCL).

Downloading the code

The overall project can be downloaded as a zip file from:

https://bitbucket.org/Holmes/prover/src

Formulae for F2 and F4.

The axioms for F2 and F4 are at this gist.

https://gist.github.com/naveensundarg/b51f9cfa4541933fc18fe571f77fe497

Formulae for F1 and F3 and the De Se condition.

https://gist.github.com/naveensundarg/3c4c895ec49ce21efd74408f58472b56

Running the Simulations

Running F2 and F4

You need Common Lisp for this. From the base directory, execute the following commands.

https://gist.github.com/naveensundarg/0aa27047b95bb0b199f30007dd8ef375

Running F1 and F3

See instructions here: https://gist.github.com/IJCAI2017-3841/82a49845703ef3dc51db2389d306b760

ShadowProver Internals

An overview of the prover can be found here:

https://drive.google.com/file/d/0B9Vb2O21ibhaZTNLd21wd21adjg/view?usp=sharing

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment