Lcfprop (Calculemus)

Lcfprop Module

Namespace: Calculemus
Assembly: Calculemus.dll

Propositional logic by inference.

Functions and values

Function or value	Description
`add_assum p th` Full Usage: `add_assum p th` Parameters: p : `formula<fol>` th : `thm` Returns: `thm`	p : `formula<fol>` th : `thm` Returns: `thm`
`and_left p q` Full Usage: `and_left p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`and_pair p q` Full Usage: `and_pair p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`and_right p q` Full Usage: `and_right p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`conjths fm` Full Usage: `conjths fm` Parameters: fm : `formula<fol>` Returns: `thm list`	fm : `formula<fol>` Returns: `thm list`
`contrapos th` Full Usage: `contrapos th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`eliminate_connective fm` Full Usage: `eliminate_connective fm` Parameters: fm : `formula<fol>` Returns: `thm`	fm : `formula<fol>` Returns: `thm`
`ex_falso p` Full Usage: `ex_falso p` Parameters: p : `formula<fol>` Returns: `thm`	p : `formula<fol>` Returns: `thm`
`expand_connective fm` Full Usage: `expand_connective fm` Parameters: fm : `formula<fol>` Returns: `thm`	fm : `formula<fol>` Returns: `thm`
`iff_def p q` Full Usage: `iff_def p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`iff_imp1 th` Full Usage: `iff_imp1 th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`iff_imp2 th` Full Usage: `iff_imp2 th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`imp_add_assum p th` Full Usage: `imp_add_assum p th` Parameters: p : `formula<fol>` th : `thm` Returns: `thm`	p : `formula<fol>` th : `thm` Returns: `thm`
`imp_add_concl r th` Full Usage: `imp_add_concl r th` Parameters: r : `formula<fol>` th : `thm` Returns: `thm`	r : `formula<fol>` th : `thm` Returns: `thm`
`imp_antisym th1 th2` Full Usage: `imp_antisym th1 th2` Parameters: th1 : `thm` th2 : `thm` Returns: `thm`	th1 : `thm` th2 : `thm` Returns: `thm`
`imp_contr p q` Full Usage: `imp_contr p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`imp_false_conseqs p q` Full Usage: `imp_false_conseqs p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm list`	p : `formula<fol>` q : `formula<fol>` Returns: `thm list`
`imp_false_rule th` Full Usage: `imp_false_rule th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`imp_front n th` Full Usage: `imp_front n th` Parameters: n : `int` th : `thm` Returns: `thm`	n : `int` th : `thm` Returns: `thm`
`imp_front_th n fm` Full Usage: `imp_front_th n fm` Parameters: n : `int` fm : `formula<fol>` Returns: `thm`	n : `int` fm : `formula<fol>` Returns: `thm`
`imp_insert q th` Full Usage: `imp_insert q th` Parameters: q : `formula<fol>` th : `thm` Returns: `thm`	q : `formula<fol>` th : `thm` Returns: `thm`
`imp_mono_th p p' q q'` Full Usage: `imp_mono_th p p' q q'` Parameters: p : `formula<fol>` p' : `formula<fol>` q : `formula<fol>` q' : `formula<fol>` Returns: `thm`	p : `formula<fol>` p' : `formula<fol>` q : `formula<fol>` q' : `formula<fol>` Returns: `thm`
`imp_refl p` Full Usage: `imp_refl p` Parameters: p : `formula<fol>` Returns: `thm`	p : `formula<fol>` Returns: `thm`
`imp_swap th` Full Usage: `imp_swap th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`imp_swap2 th` Full Usage: `imp_swap2 th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`imp_swap_th p q r` Full Usage: `imp_swap_th p q r` Parameters: p : `formula<fol>` q : `formula<fol>` r : `formula<fol>` Returns: `thm`	p : `formula<fol>` q : `formula<fol>` r : `formula<fol>` Returns: `thm`
`imp_trans th1 th2` Full Usage: `imp_trans th1 th2` Parameters: th1 : `thm` th2 : `thm` Returns: `thm`	th1 : `thm` th2 : `thm` Returns: `thm`
`imp_trans2 th1 th2` Full Usage: `imp_trans2 th1 th2` Parameters: th1 : `thm` th2 : `thm` Returns: `thm`	th1 : `thm` th2 : `thm` Returns: `thm`
`imp_trans_chain ths th` Full Usage: `imp_trans_chain ths th` Parameters: ths : `thm list` th : `thm` Returns: `thm`	ths : `thm list` th : `thm` Returns: `thm`
`imp_trans_th p q r` Full Usage: `imp_trans_th p q r` Parameters: p : `formula<fol>` q : `formula<fol>` r : `formula<fol>` Returns: `thm`	p : `formula<fol>` q : `formula<fol>` r : `formula<fol>` Returns: `thm`
`imp_true_rule th1 th2` Full Usage: `imp_true_rule th1 th2` Parameters: th1 : `thm` th2 : `thm` Returns: `thm`	th1 : `thm` th2 : `thm` Returns: `thm`
`imp_truefalse p q` Full Usage: `imp_truefalse p q` Parameters: p : `formula<fol>` q : `formula<fol>` Returns: `thm`	p : `formula<fol>` q : `formula<fol>` Returns: `thm`
`imp_unduplicate th` Full Usage: `imp_unduplicate th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`lcfptab fms lits` Full Usage: `lcfptab fms lits` Parameters: fms : `formula<fol> list` lits : `formula<fol> list` Returns: `thm`	fms : `formula<fol> list` lits : `formula<fol> list` Returns: `thm`
`lcftaut p` Full Usage: `lcftaut p` Parameters: p : `formula<fol>` Returns: `thm`	p : `formula<fol>` Returns: `thm`
`negatef fm` Full Usage: `negatef fm` Parameters: fm : `formula<'a>` Returns: `formula<'a>`	fm : `formula<'a>` Returns: `formula<'a>`
`negativef fm` Full Usage: `negativef fm` Parameters: fm : `formula<'a>` Returns: `bool`	fm : `formula<'a>` Returns: `bool`
`right_doubleneg th` Full Usage: `right_doubleneg th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`right_mp ith th` Full Usage: `right_mp ith th` Parameters: ith : `thm` th : `thm` Returns: `thm`	ith : `thm` th : `thm` Returns: `thm`
`shunt th` Full Usage: `shunt th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`
`truth` Full Usage: `truth` Returns: `thm`	Returns: `thm`
`unshunt th` Full Usage: `unshunt th` Parameters: th : `thm` Returns: `thm`	th : `thm` Returns: `thm`