Annotated Formulae
language(name, role, formula, source, [useful_info]).
Languages
- thf - Typed Higher-order Form
- tff - Typed First-order Form
- fof - First Order Form
- cnf - Clause Normal Form
Roles
- axiom - accepted, without proof, as a basis for reasoning
- conjecture - to all be proven from the axiom(-like)
formulae
- negated_conjecture - formed from negation of a
conjecture
- See BNF for others
Logical Formula
- Use a consistent, easily understood notation
Source
- file(file_name, formula_name)
- inference(rule_name, useful_info, [parent_list])
Useful Information
- Prolog-like terms for application data