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 873 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
invalid "Failure"
12
invalid "No Proof Found"
13
14
15
16
17
18
19
20
21
22
23
24
25

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

26
27
transformation "encoding_decorate"

28
29
(* TODO : transformation to eliminate types *)

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

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:
*)
45
46
(* vim:syntax=ocaml
*)