tptp.drv 954 Bytes
Newer Older
1
2
3

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

4
5
6
prelude "% this is a why prelude for tptp solvers
fof(two_constants, axiom, ~ ('0' = '1')).
"
7
8
9
10
11

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

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

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

30
transformation "explicit_polymorphism"
31

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
*)