Semantic Tableaux proof method for predicate logic
January 16th, 2004
View as: 
A backward-chaining proof method for predicate logic, motivated by proof by contradiction rather than deduction. Description of the semantic tableau structure and rules, with suggested order of application. Also includes worked examples and a proof of correctness and completeness (with reference to Gödel’s theorems).