Catalogue of Artificial Intelligence Techniques
Categories: Inference and Reasoning
Author(s): Alan Smaill
A method of presenting a logic invented by Gentzen in which statements are made in the form:
one of the propositions holds. A logic is characterised by giving basic sequents as axioms and then allowing further sequents to be derived using rules of inference, typically associated with the introduction and elimination of the logical symbols of the language on either side of the arrow; for example, the rule for introducing a disjunction is:
- Gallier, J.H., Logic for computer science: foundations of
automatic theorem proving
, Harper & Row, New York and London, 1986.