Constructive Pruning-Based Completeness Proofs for K
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (247 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (26 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (56 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |
Global Index
A
axDN [constructor, in K.K_def]axK [constructor, in K.K_def]
axN [constructor, in K.K_def]
axS [constructor, in K.K_def]
ax_lcons [lemma, in K.hilbert_ref]
B
baseP [lemma, in K.hilbert_ref]base0P [lemma, in K.hilbert_ref]
body [definition, in K.K_def]
box_request [lemma, in K.K_def]
C
cAX [definition, in K.K_def]cEX [definition, in K.K_def]
Characterizations [section, in K.K_def]
Characterizations.e [variable, in K.K_def]
Characterizations.X [variable, in K.K_def]
clause [definition, in K.K_def]
closed_sfc [lemma, in K.K_def]
cls [projection, in K.demo]
cmodel [record, in K.K_def]
CModel [constructor, in K.K_def]
coref [definition, in K.demo]
corefD1 [lemma, in K.demo]
coref_DD [lemma, in K.demo]
D
dbound [projection, in K.universal_model]DD [definition, in K.demo]
DD_canonical [lemma, in K.hilbert_ref]
DD_supp [lemma, in K.hilbert_ref]
DD_supp_sat [lemma, in K.hilbert_ref]
DD_canonical [lemma, in K.results]
DD_refute [lemma, in K.demo]
demo [record, in K.demo]
Demo [constructor, in K.demo]
demo [library]
demoD0 [projection, in K.demo]
demoD1 [projection, in K.demo]
dlabel [projection, in K.universal_model]
DM [constructor, in K.universal_model]
dmodel [record, in K.universal_model]
dmodelP [lemma, in K.universal_model]
dstate [projection, in K.universal_model]
dtrans [projection, in K.universal_model]
dtransP [projection, in K.universal_model]
D0 [definition, in K.demo]
D1 [definition, in K.demo]
E
eq_form_dec [lemma, in K.K_def]eval [definition, in K.K_def]
evalb [definition, in K.K_def]
evald [definition, in K.universal_model]
evaldP [lemma, in K.universal_model]
evalP [lemma, in K.K_def]
ex_fc [lemma, in K.gentzen]
F
fAX [constructor, in K.K_def]fF [constructor, in K.K_def]
fImp [constructor, in K.K_def]
FiniteModels [section, in K.K_def]
FiniteModels.M [variable, in K.K_def]
fin_modelP [lemma, in K.K_def]
flabel [projection, in K.K_def]
fmodel [record, in K.K_def]
FModel [constructor, in K.K_def]
form [inductive, in K.K_def]
formChoice [module, in K.K_def]
formChoice.pickle [definition, in K.K_def]
formChoice.pickleP [lemma, in K.K_def]
formChoice.unpickle [definition, in K.K_def]
form_slClass [definition, in K.K_def]
form_choiceMixin [definition, in K.K_def]
form_countMixin [definition, in K.K_def]
form_eqMixin [definition, in K.K_def]
fstate [projection, in K.K_def]
ftrans [projection, in K.K_def]
fV [constructor, in K.K_def]
f_size [definition, in K.K_def]
f_weight [definition, in K.K_def]
G
gen [inductive, in K.gentzen]genN_supp [lemma, in K.universal_model]
gentzen [library]
gen_lcons [lemma, in K.universal_model]
gen_decP [lemma, in K.universal_model]
gen_dec [lemma, in K.results]
gen_correctness [lemma, in K.results]
gen_completeness [lemma, in K.results]
gen_dec [lemma, in K.gentzen]
gen_correctness [lemma, in K.gentzen]
gen_completeness [lemma, in K.gentzen]
gen_of_ref [lemma, in K.gentzen]
gen_ref_sound [lemma, in K.gentzen]
gen_hsound [lemma, in K.gentzen]
gen_AXn [constructor, in K.gentzen]
gen_In [constructor, in K.gentzen]
gen_Ip [constructor, in K.gentzen]
gen_p [constructor, in K.gentzen]
gen_F [constructor, in K.gentzen]
H
Hilbert [section, in K.K_def]hilbert_ref [library]
_ ---> _ [notation, in K.K_def]
href [definition, in K.hilbert_ref]
href_of [lemma, in K.hilbert_ref]
href_R1 [lemma, in K.hilbert_ref]
href_R2 [lemma, in K.hilbert_ref]
href_sound [lemma, in K.K_def]
I
informative_completeness [lemma, in K.hilbert_ref]informative_completeness [lemma, in K.results]
interp [definition, in K.K_def]
inU_sfc [lemma, in K.K_def]
isBox [definition, in K.K_def]
isBoxP [lemma, in K.K_def]
isBox_false [constructor, in K.K_def]
isBox_true [constructor, in K.K_def]
isBox_spec [inductive, in K.K_def]
isDia [definition, in K.K_def]
isDiaP [lemma, in K.K_def]
isDia_false [constructor, in K.K_def]
isDia_true [constructor, in K.K_def]
isDia_spec [inductive, in K.K_def]
K
K_def [library]L
label [projection, in K.K_def]LCF [lemma, in K.demo]
lcons [definition, in K.K_def]
lcons_gen [lemma, in K.gentzen]
ldec [definition, in K.K_def]
literal [definition, in K.K_def]
M
Mlabel [definition, in K.demo]ModelExistience [section, in K.demo]
ModelExistience.S [variable, in K.demo]
modelP [projection, in K.K_def]
model_of_dmodel [definition, in K.universal_model]
model_of [definition, in K.demo]
Mtrans [definition, in K.demo]
Mtype [definition, in K.demo]
P
pcond [definition, in K.demo]prune_D1 [lemma, in K.demo]
prune_D0 [lemma, in K.demo]
Pruning [section, in K.demo]
Pruning.F [variable, in K.demo]
Pruning.sfc_F [variable, in K.demo]
prv [inductive, in K.K_def]
prv_dec [lemma, in K.hilbert_ref]
prv_dec [lemma, in K.results]
R
R [definition, in K.K_def]RE [lemma, in K.K_def]
ref [inductive, in K.demo]
RefPred [section, in K.hilbert_ref]
RefPred [section, in K.gentzen]
RefPred.ContextRefutations [section, in K.hilbert_ref]
RefPred.ContextRefutations.coref_S [variable, in K.hilbert_ref]
RefPred.ContextRefutations.S [variable, in K.hilbert_ref]
RefPred.F [variable, in K.hilbert_ref]
RefPred.F [variable, in K.gentzen]
RefPred.sfc_F [variable, in K.hilbert_ref]
RefPred.sfc_F [variable, in K.gentzen]
refutation_completeness [lemma, in K.demo]
ref_R2 [lemma, in K.gentzen]
ref_R1 [lemma, in K.gentzen]
ref_coref [lemma, in K.gentzen]
ref_R0 [lemma, in K.gentzen]
results [library]
RinU [lemma, in K.K_def]
rMP [constructor, in K.K_def]
rNec [constructor, in K.K_def]
Rpos [lemma, in K.K_def]
rtrans [definition, in K.demo]
RU [lemma, in K.K_def]
R0 [lemma, in K.K_def]
R1 [lemma, in K.K_def]
R1 [constructor, in K.demo]
R1inU [lemma, in K.demo]
R2 [constructor, in K.demo]
S
sat [definition, in K.K_def]satA [lemma, in K.K_def]
sat_cons [lemma, in K.universal_model]
sat_dec [lemma, in K.hilbert_ref]
sat_dec [lemma, in K.results]
sfc [definition, in K.K_def]
sfcU [lemma, in K.K_def]
sfc_bigcup [lemma, in K.K_def]
sfc_ssub [lemma, in K.K_def]
sform [definition, in K.K_def]
sf_ssub [lemma, in K.K_def]
sf_closed'_mon [lemma, in K.K_def]
sf_closed [definition, in K.K_def]
sf_closed' [definition, in K.K_def]
size_ssub [lemma, in K.K_def]
small_models [lemma, in K.hilbert_ref]
small_models [lemma, in K.results]
soundness [lemma, in K.K_def]
soundness [lemma, in K.results]
ssub [definition, in K.K_def]
ssub_refl [lemma, in K.K_def]
ssub' [definition, in K.K_def]
ssub'_refl [lemma, in K.K_def]
stable [definition, in K.K_def]
state [projection, in K.K_def]
sts_of [projection, in K.K_def]
sub_sfc [lemma, in K.K_def]
supp [definition, in K.K_def]
suppC1 [lemma, in K.K_def]
support_sat [lemma, in K.hilbert_ref]
support_sat [lemma, in K.results]
supp_eval [lemma, in K.universal_model]
supp_lit [lemma, in K.K_def]
supp_mon [lemma, in K.K_def]
supp_eval [lemma, in K.demo]
sweight_lit [lemma, in K.K_def]
S0 [abbreviation, in K.hilbert_ref]
S0 [definition, in K.demo]
S0 [abbreviation, in K.gentzen]
T
trans [projection, in K.K_def]ts [record, in K.K_def]
TS [constructor, in K.K_def]
ts_of_dmodel [definition, in K.universal_model]
U
U [abbreviation, in K.hilbert_ref]U [definition, in K.demo]
U [abbreviation, in K.gentzen]
UM [definition, in K.universal_model]
UMd [definition, in K.universal_model]
UMLabel [definition, in K.universal_model]
UMP [lemma, in K.universal_model]
UMType [definition, in K.universal_model]
UM_universal [lemma, in K.universal_model]
UM_trans_D [lemma, in K.universal_model]
UM_trans_R [lemma, in K.universal_model]
UM_trans_bound [lemma, in K.universal_model]
UM_bound [definition, in K.universal_model]
UM_trans [definition, in K.universal_model]
UM_select_correct [lemma, in K.universal_model]
UM_select [definition, in K.universal_model]
UM_default [definition, in K.universal_model]
UM_default_proof [lemma, in K.universal_model]
UM_universal [lemma, in K.results]
UniversalModel [section, in K.universal_model]
universal_model [library]
V
valid [definition, in K.K_def]valid_dec [lemma, in K.hilbert_ref]
valid_dec [lemma, in K.results]
var [definition, in K.K_def]
X
xaf [abbreviation, in K.hilbert_ref]xaf [abbreviation, in K.gentzen]
XM_required [lemma, in K.K_def]
xm_soundness [lemma, in K.K_def]
XM_required [lemma, in K.results]
xm_soundness [lemma, in K.results]
other
_ |> _ [notation, in K.K_def]_ |> _ ^- [notation, in K.K_def]
_ |> _ ^+ [notation, in K.K_def]
_ |> _ ^ _ [notation, in K.K_def]
_ ^+ [notation, in K.K_def]
_ ^- [notation, in K.K_def]
Notation Index
H
_ ---> _ [in K.K_def]other
_ |> _ [in K.K_def]_ |> _ ^- [in K.K_def]
_ |> _ ^+ [in K.K_def]
_ |> _ ^ _ [in K.K_def]
_ ^+ [in K.K_def]
_ ^- [in K.K_def]
Module Index
F
formChoice [in K.K_def]Variable Index
C
Characterizations.e [in K.K_def]Characterizations.X [in K.K_def]
F
FiniteModels.M [in K.K_def]M
ModelExistience.S [in K.demo]P
Pruning.F [in K.demo]Pruning.sfc_F [in K.demo]
R
RefPred.ContextRefutations.coref_S [in K.hilbert_ref]RefPred.ContextRefutations.S [in K.hilbert_ref]
RefPred.F [in K.hilbert_ref]
RefPred.F [in K.gentzen]
RefPred.sfc_F [in K.hilbert_ref]
RefPred.sfc_F [in K.gentzen]
Library Index
D
demoG
gentzenH
hilbert_refK
K_defR
resultsU
universal_modelLemma Index
A
ax_lcons [in K.hilbert_ref]B
baseP [in K.hilbert_ref]base0P [in K.hilbert_ref]
box_request [in K.K_def]
C
closed_sfc [in K.K_def]corefD1 [in K.demo]
coref_DD [in K.demo]
D
DD_canonical [in K.hilbert_ref]DD_supp [in K.hilbert_ref]
DD_supp_sat [in K.hilbert_ref]
DD_canonical [in K.results]
DD_refute [in K.demo]
dmodelP [in K.universal_model]
E
eq_form_dec [in K.K_def]evaldP [in K.universal_model]
evalP [in K.K_def]
ex_fc [in K.gentzen]
F
fin_modelP [in K.K_def]formChoice.pickleP [in K.K_def]
G
genN_supp [in K.universal_model]gen_lcons [in K.universal_model]
gen_decP [in K.universal_model]
gen_dec [in K.results]
gen_correctness [in K.results]
gen_completeness [in K.results]
gen_dec [in K.gentzen]
gen_correctness [in K.gentzen]
gen_completeness [in K.gentzen]
gen_of_ref [in K.gentzen]
gen_ref_sound [in K.gentzen]
gen_hsound [in K.gentzen]
H
href_of [in K.hilbert_ref]href_R1 [in K.hilbert_ref]
href_R2 [in K.hilbert_ref]
href_sound [in K.K_def]
I
informative_completeness [in K.hilbert_ref]informative_completeness [in K.results]
inU_sfc [in K.K_def]
isBoxP [in K.K_def]
isDiaP [in K.K_def]
L
LCF [in K.demo]lcons_gen [in K.gentzen]
P
prune_D1 [in K.demo]prune_D0 [in K.demo]
prv_dec [in K.hilbert_ref]
prv_dec [in K.results]
R
RE [in K.K_def]refutation_completeness [in K.demo]
ref_R2 [in K.gentzen]
ref_R1 [in K.gentzen]
ref_coref [in K.gentzen]
ref_R0 [in K.gentzen]
RinU [in K.K_def]
Rpos [in K.K_def]
RU [in K.K_def]
R0 [in K.K_def]
R1 [in K.K_def]
R1inU [in K.demo]
S
satA [in K.K_def]sat_cons [in K.universal_model]
sat_dec [in K.hilbert_ref]
sat_dec [in K.results]
sfcU [in K.K_def]
sfc_bigcup [in K.K_def]
sfc_ssub [in K.K_def]
sf_ssub [in K.K_def]
sf_closed'_mon [in K.K_def]
size_ssub [in K.K_def]
small_models [in K.hilbert_ref]
small_models [in K.results]
soundness [in K.K_def]
soundness [in K.results]
ssub_refl [in K.K_def]
ssub'_refl [in K.K_def]
sub_sfc [in K.K_def]
suppC1 [in K.K_def]
support_sat [in K.hilbert_ref]
support_sat [in K.results]
supp_eval [in K.universal_model]
supp_lit [in K.K_def]
supp_mon [in K.K_def]
supp_eval [in K.demo]
sweight_lit [in K.K_def]
U
UMP [in K.universal_model]UM_universal [in K.universal_model]
UM_trans_D [in K.universal_model]
UM_trans_R [in K.universal_model]
UM_trans_bound [in K.universal_model]
UM_select_correct [in K.universal_model]
UM_default_proof [in K.universal_model]
UM_universal [in K.results]
V
valid_dec [in K.hilbert_ref]valid_dec [in K.results]
X
XM_required [in K.K_def]xm_soundness [in K.K_def]
XM_required [in K.results]
xm_soundness [in K.results]
Constructor Index
A
axDN [in K.K_def]axK [in K.K_def]
axN [in K.K_def]
axS [in K.K_def]
C
CModel [in K.K_def]D
Demo [in K.demo]DM [in K.universal_model]
F
fAX [in K.K_def]fF [in K.K_def]
fImp [in K.K_def]
FModel [in K.K_def]
fV [in K.K_def]
G
gen_AXn [in K.gentzen]gen_In [in K.gentzen]
gen_Ip [in K.gentzen]
gen_p [in K.gentzen]
gen_F [in K.gentzen]
I
isBox_false [in K.K_def]isBox_true [in K.K_def]
isDia_false [in K.K_def]
isDia_true [in K.K_def]
R
rMP [in K.K_def]rNec [in K.K_def]
R1 [in K.demo]
R2 [in K.demo]
T
TS [in K.K_def]Projection Index
C
cls [in K.demo]D
dbound [in K.universal_model]demoD0 [in K.demo]
demoD1 [in K.demo]
dlabel [in K.universal_model]
dstate [in K.universal_model]
dtrans [in K.universal_model]
dtransP [in K.universal_model]
F
flabel [in K.K_def]fstate [in K.K_def]
ftrans [in K.K_def]
L
label [in K.K_def]M
modelP [in K.K_def]S
state [in K.K_def]sts_of [in K.K_def]
T
trans [in K.K_def]Inductive Index
F
form [in K.K_def]G
gen [in K.gentzen]I
isBox_spec [in K.K_def]isDia_spec [in K.K_def]
P
prv [in K.K_def]R
ref [in K.demo]Section Index
C
Characterizations [in K.K_def]F
FiniteModels [in K.K_def]H
Hilbert [in K.K_def]M
ModelExistience [in K.demo]P
Pruning [in K.demo]R
RefPred [in K.hilbert_ref]RefPred [in K.gentzen]
RefPred.ContextRefutations [in K.hilbert_ref]
U
UniversalModel [in K.universal_model]Abbreviation Index
S
S0 [in K.hilbert_ref]S0 [in K.gentzen]
U
U [in K.hilbert_ref]U [in K.gentzen]
X
xaf [in K.hilbert_ref]xaf [in K.gentzen]
Definition Index
B
body [in K.K_def]C
cAX [in K.K_def]cEX [in K.K_def]
clause [in K.K_def]
coref [in K.demo]
D
DD [in K.demo]D0 [in K.demo]
D1 [in K.demo]
E
eval [in K.K_def]evalb [in K.K_def]
evald [in K.universal_model]
F
formChoice.pickle [in K.K_def]formChoice.unpickle [in K.K_def]
form_slClass [in K.K_def]
form_choiceMixin [in K.K_def]
form_countMixin [in K.K_def]
form_eqMixin [in K.K_def]
f_size [in K.K_def]
f_weight [in K.K_def]
H
href [in K.hilbert_ref]I
interp [in K.K_def]isBox [in K.K_def]
isDia [in K.K_def]
L
lcons [in K.K_def]ldec [in K.K_def]
literal [in K.K_def]
M
Mlabel [in K.demo]model_of_dmodel [in K.universal_model]
model_of [in K.demo]
Mtrans [in K.demo]
Mtype [in K.demo]
P
pcond [in K.demo]R
R [in K.K_def]rtrans [in K.demo]
S
sat [in K.K_def]sfc [in K.K_def]
sform [in K.K_def]
sf_closed [in K.K_def]
sf_closed' [in K.K_def]
ssub [in K.K_def]
ssub' [in K.K_def]
stable [in K.K_def]
supp [in K.K_def]
S0 [in K.demo]
T
ts_of_dmodel [in K.universal_model]U
U [in K.demo]UM [in K.universal_model]
UMd [in K.universal_model]
UMLabel [in K.universal_model]
UMType [in K.universal_model]
UM_bound [in K.universal_model]
UM_trans [in K.universal_model]
UM_select [in K.universal_model]
UM_default [in K.universal_model]
V
valid [in K.K_def]var [in K.K_def]
Record Index
C
cmodel [in K.K_def]D
demo [in K.demo]dmodel [in K.universal_model]
F
fmodel [in K.K_def]T
ts [in K.K_def]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (247 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (26 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (16 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (56 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 entries) |