| author | paulson <lp15@cam.ac.uk> |
| Wed, 27 Oct 2021 11:47:42 +0100 | |
| changeset 74598 | 5d91897a8e54 |
| parent 63960 | 3daf02070be5 |
| permissions | -rw-r--r-- |
|
63960
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
1 |
(* Title: Tools/Argo/argo_common.ML |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
3 |
|
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
4 |
Common infrastructure for the decision procedures of Argo. |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
5 |
*) |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
6 |
|
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
7 |
signature ARGO_COMMON = |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
8 |
sig |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
9 |
type literal = Argo_Lit.literal * Argo_Proof.proof option |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
10 |
datatype 'a implied = Implied of 'a list | Conflict of Argo_Cls.clause |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
11 |
end |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
12 |
|
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
13 |
structure Argo_Common: ARGO_COMMON = |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
14 |
struct |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
15 |
|
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
16 |
type literal = Argo_Lit.literal * Argo_Proof.proof option |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
17 |
(* Implied new knowledge accompanied with an optional proof. If there is no proof, |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
18 |
the literal is to be treated hypothetically. If there is a proof, the literal is |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
19 |
to be treated as uni clause. *) |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
20 |
|
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
21 |
datatype 'a implied = Implied of 'a list | Conflict of Argo_Cls.clause |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
22 |
(* A result of a step of a decision procedure, either an implication of new knowledge |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
23 |
or clause whose literals are known to be false. *) |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
24 |
|
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
25 |
end |