#
8c5d9dd7 |
|
08-Aug-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement new special syntax for Datatype General form is Datatype: ty1 = Cnname1 ty2 ty3 | Cnname2 ty...; ty2 = ... ; ... End Illustrate in folLangScript.sml. Thanks to Scott Owens for the suggestion.
|
#
d534a500 |
|
07-Aug-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Complete port of HOL Light FOL compactness material Also add a finite entailment property: INFINITE 𝕌(:α) ⇒ (entails (:α) Γ ϕ ⇔ ∃Γ₀. FINITE Γ₀ ∧ Γ₀ ⊆ Γ ∧ entails (:α) Γ₀ ϕ) You only need a finite number of hypotheses to get to a conclusion. This is obvious if you have a proof system, but is true thanks to compactness if you are just working with models.
|
#
cfe09cf1 |
|
31-Jul-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More progress with FOL compactness port
|
#
922e2366 |
|
29-Jul-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Progress with port of HOL Light compactness etc theories
|
#
97dbc36b |
|
29-Jul-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Start port of material about f.o. compactness from HOL Light See commit https://github.com/jrh13/hol-light/commit/013324af7ff715346383fb963d323138cf011732 Thanks to John for making this available (some of it is behind his TPHOLs 1998 paper.)
|