Catalogue of Artificial Intelligence Techniques


Jump to: Top | Entry | References | Comments

View Maths as: Images | MathML

Sequent Calculus

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:

A1,A2,... An  B1,B2,... Bm

where the sequent sign ` ' indicates that given all the propositions Ai

one of the propositions Bj 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:

Γ  Θ,P,Q

Γ  Θ, P  Q¯

where Γ and Θ represent an arbitrary number of propositions. One of the advantages of sequent calculus over, say, Natural Deduction is the ease with which proofs can be manipulated (e.g., Gentzen's work on proof theory).



Add Comment

No comments.