ClassicalProp jlc NuprlLIB Doc

Sections needed for ClassicalProp_jlc

ClassicalProp jlcJim Caldwell's development of Classical Propositional Logic.
decidability
normalizationThe normalization lemma.
elimination
sequent valid
full sequent assignment
sequent sat lemmas
sequent falsification
sequent satisfaction
sequent rank
formula list
sequent equality
sequent
formula validity
full assignment
sat lemmas
formula equality
formula falsification
formula satisfaction
formula rank
valuation
KleeneKleene 3-valued truth connectives.
assignment
ThreeType of 3-truth-values
formulaPropositional formula structure.
var jlc
list 3 jlcMore on Lists
core 3 jlcVarious facts about Propositional Operators
discrete jlcBasics of Discrete Types
bool 2 jlcA few basic facts about asserting Bools and Bool Equalities
lambda jlcCurrying functions and Explicitly expressing recursion.
list 1
int 2Defines mod, floor, max and min functions over the integers. Lemmas concern basic properties of arithmetic functions over integers, and induction principles.
rfunction 1
prog 1
sqequal 1
quot 1Support lemmas for quotient type.
rel 1Common properties of binary relations.
unionNon canonical functions (isl, outl, outr) for union type.
bool 1Definitions, theorems and tactics for the boolean type and boolean-related expressions.
int 1Integer inequalities, subtypes, and induction lemmas for subtypes.
well fndWell-founded predicate. Rank induction lemmas and tactics.
fun 1Polymorphic identity and composition functions. Lemmas covering properties such as injectivity and surjectivity.
coreSome basic concepts defined type-theoretically.