Lcf (Calculemus)

Lcf Module

Namespace: Calculemus
Assembly: Calculemus.dll

LCF-style system for first order logic.

Basic first order deductive system.

This is based on Tarski's trick for avoiding use of a substitution primitive. It seems about the simplest possible system we could use.

Nested modules

Modules	Description
ProofSystem	The Core LCF proof system The core proof system is the minimum set of inference rules and/or axioms sound and complete with respect to the defined semantics.

Functions and values

Function or value	Description
`fprint_thm sw th` Full Usage: `fprint_thm sw th` Parameters: sw : `TextWriter` th : `thm`	Prints a theorem using a TextWriter. sw : `TextWriter` th : `thm`
`free_in t fm` Full Usage: `free_in t fm` Parameters: t : `term` fm : `formula<fol>` Returns: `bool`	checks whether a term t occurs free in a formula fm t : `term` fm : `formula<fol>` Returns: `bool`
`occurs_in s t` Full Usage: `occurs_in s t` Parameters: s : `term` t : `term` Returns: `bool`	checks whether a term s occurs as a sub-term of another term t s : `term` t : `term` Returns: `bool`
`print_thm th` Full Usage: `print_thm th` Parameters: th : `thm` Modifiers: inline	A printer for theorems th : `thm`
`sprint_thm th` Full Usage: `sprint_thm th` Parameters: th : `thm` Returns: `string` Modifiers: inline	Theorem to string th : `thm` Returns: `string`