1 (* ========================================================================= *) |
1 (* ========================================================================= *) |
2 (* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES *) |
2 (* CNF PROBLEMS *) |
3 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *) |
3 (* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *) |
4 (* ========================================================================= *) |
4 (* ========================================================================= *) |
5 |
5 |
6 signature Problem = |
6 signature Problem = |
7 sig |
7 sig |
8 |
8 |
9 (* ------------------------------------------------------------------------- *) |
9 (* ------------------------------------------------------------------------- *) |
10 (* Problems. *) |
10 (* Problems. *) |
11 (* ------------------------------------------------------------------------- *) |
11 (* ------------------------------------------------------------------------- *) |
12 |
12 |
13 type problem = Thm.clause list |
13 type problem = |
|
14 {axioms : Thm.clause list, |
|
15 conjecture : Thm.clause list} |
14 |
16 |
15 val size : problem -> {clauses : int, |
17 val size : problem -> {clauses : int, |
16 literals : int, |
18 literals : int, |
17 symbols : int, |
19 symbols : int, |
18 typedSymbols : int} |
20 typedSymbols : int} |
19 |
21 |
20 val fromGoal : Formula.formula -> problem list |
22 val freeVars : problem -> NameSet.set |
21 |
23 |
22 val toClauses : problem -> Formula.formula |
24 val toClauses : problem -> Thm.clause list |
|
25 |
|
26 val toFormula : problem -> Formula.formula |
|
27 |
|
28 val toGoal : problem -> Formula.formula |
23 |
29 |
24 val toString : problem -> string |
30 val toString : problem -> string |
25 |
31 |
26 (* ------------------------------------------------------------------------- *) |
32 (* ------------------------------------------------------------------------- *) |
27 (* Categorizing problems. *) |
33 (* Categorizing problems. *) |