 A deduction calculus consists of a set of logical axioms and a collection of deduction rules for deriving new formulas from previously derived formulas. Solving a problem in the program’s problem domain then really means establishing a particular formula α—the problem’s conclusion—from the extended set Γ consisting of the logical axioms, the domain axioms, and the problem assumptions. That is, the program needs to determine if Γ entails α, Γ⊨ α. How the program goes about establishing this semantic fact depends, of course, on the calculus it implements. Some programs may take a very direct route and attempt to establish that Γ ⊨ α by actually constructing a step-by-step proof of α from Γ. If successful, this shows of course that Γ derives—proves—α, a fact we denote by writing Γ ⊢ α. Other reasoning programs may instead opt for a more indirect approach and try to establish that Γ ⊨ α by showing that Γ ∪ {~α} is inconsistent which, in turn, is shown by deriving a contradiction, ⊥, from the set Γ ∪ {~α}. Automated systems that implement the former approach include natural deduction systems; the latter approach is used by systems based on resolution, sequent deduction, and matrix connection methods.