Sequent calculus

Sequent calculus

Logic

Published in Jay Liebowitz, The Handbook of Applied Expert Systems, 2019

Theorem provers use a proof procedure such as resolution, sequent, calculus, tableaux, mathematical induction, etc. to prove that a formula can be deduced from a knowledge base using some type of logic. Typically, they use backward-chaining reasoning, search control methods, and heuristics to prune the search space generated by the potential application of inference rules. OTTER and NQTHM are two of the best-known theorem provers. OTTER is based on resolution and NQTHM is based on mathematical induction. Both have been used extensibly in the construction of intelligent development environments for the design of software and hardware systems.

Structural proof theory for first-order weak Kleene logics

View Article

Journal Information

Published in Journal of Applied Non-Classical Logics, 2020

Andreas Fjellstad

In addition to possessing desirable features from the perspective of structural proof theory, the sequent calculus also offers a straightforward representation of a valid inference of classical logic. A completeness theorem will tell us that is derivable if and only if Γ entails Δ according to first-order classical logic as defined for the language in question. This might seem like a triviality, but the literature is rife with sequent calculi in which the connection between a derivable sequent and a valid inference is more obscure.

Explore chapters and articles related to this topic

Logic

Structural proof theory for first-order weak Kleene logics