Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

tptp.drv 954 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"

Simon Cruanes's avatar
Simon Cruanes committed
28
transformation "polymorphic_to_untyped"
29

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