tptp.drv 949 Bytes
Newer Older
1
2
3
4
5
6
7
8
9

(* Why driver for tptp first-order logic solvers *)

prelude "% this is a prelude for tptp solvers"

printer "tptp"
filename "%f-%t-%g.p"

valid "Proof found"
10
valid "Completion found"
11
12
13
14
fail "Failure" "Failure"
unknown "No Proof Found" "Unknown"
timeout "Resource limit exceeded"
timeout "Ran out of time"
15
16
17
18
19
20
21
22
23
24
25
26
27

(* to be improved *)

transformation "simplify_recursive_definition"
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_let"

28
29
transformation "encoding_decorate"

30
31
(* TODO : transformation to eliminate types *)

32
33
34
35
36
37
38
39
40
41
42
43
44
45

theory BuiltIn
  syntax type int "Int"
  syntax type real "Real"
  syntax logic (_=_) "(%1 = %2)"
  syntax logic (_<>_) "(%1 != %2)"
end

(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
46
47
(* vim:syntax=ocaml
*)