File: README

package info (click to toggle)
acl2 8.6%2Bdfsg-2
  • links: PTS
  • area: main
  • in suites: trixie
  • size: 1,111,420 kB
  • sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (32 lines) | stat: -rw-r--r-- 963 bytes parent folder | download | duplicates (5) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
 
Nathan Wetzler
nwetzler@cs.utexas.edu
Last modified: 2013-02-14 8:31pm


The code and proofs are a work in progress.  We have provided them as
supplemental material for the Interactive Theorem Proving conference.
Code was tested with ACL2 version 6.0.


Three scripts have been provided:
build     - Will ceritfy all books
run arg1  - Will check a RAT proof file "arg1"
clean     - Will remove all certificates and logs


The ACL2 Lisp proof files are included and some descriptions are
listed below:

top.lisp - LOOK AT THIS FILE FIRST.  This contains the main events
           from the rat-checker proof without many of the ugly
           details.

rat-checker.lisp - This is the definition and proof of correctness for
                   the RAT proof checker.

rat-parser.lsp - A RAT proof file parser.

rat-1 - An sample RAT proof file.

supplemental/ - This directory contains a library of function
                definitions and theorems related to SAT.