tptp.drv 768 Bytes
Newer Older
1
(* Why driver for first-order tptp provers *)
2
3
4
5

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

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

(* 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"

25
transformation "encoding_tptp"
26
27

theory BuiltIn
28
  syntax logic (=)  "(%1 = %2)"
29
30
31
32
33
34
35
36
end

(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)