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 823 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

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

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

24
25
transformation "encoding_decorate"

26
27
(* TODO : transformation to eliminate types *)

28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

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