SNARK Documentation

SNARK tutorial

SNARK paper

github.com/nilqed/SNARK

Also see: github.com/theoremprover-museum

A simple example (wip)

some group theory ...

COO Documentation

(coo:document-system :snark)

Using from FriCAS (fricas_snark)

github.com/nilqed/fricas_snark

Overbeek Test

Example (example/overbeek-test.lisp): (snark-user::overbeek-test)

Evaluation took:
  32.517 seconds of real time
  32.456339 seconds of total run time (24.248487 user, 8.207852 system)
  [ Run times consist of 0.812 seconds GC time, and 31.645 seconds non-GC time. ]
  99.81% CPU
  23 forms interpreted
  84,285,383,422 processor cycles
  5,878,063,200 bytes consed


#||
% SZS status Unsatisfiable for /home/kfp/quicklisp/dists/quicklisp/software/snark-20160421-git/examples/LCL024-1+rm_eq_rstfp.kif
||#
:PROOF-FOUND
; End refute-file /home/kfp/quicklisp/dists/quicklisp/software/snark-20160421-git/examples/LCL024-1+rm_eq_rstfp.kif 2025-02-20T20:28:50
SNARK-USER::OVERBEEK4-1

OVERBEEK-TEST Total = 660 seconds