Attention une mise à jour du service Gitlab va être effectuée le mardi 14 décembre entre 13h30 et 14h00. 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 953 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
transformation "explicit_polymorphism"
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
*)