Automated Reasoning with Analytic Tableaux and Related Methods Book

	Proof Analysis by Resolution	1
	Using Linear Logic to Reason about Sequent Systems	2
	A Schutte-Tait Style Cut-Elimination Proof for First-Order Godel Logic	24
	Tableaux for Quantified Hybrid Logic	38
	Tableau-Based Automated Deduction for Duration Calculus	53
	Linear Time Logic, Conditioned Models, and Planning with Incomplete Knowledge	70
	A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic	85
	Model Nonmonotonic Logics Revisited: Efficient Encodings for the Basic Reasoning Tasks	100
	Tableau Calculi for the Logics of Finite k-Ary Trees	115
	A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition	130
	Implementation and Optimisation of a Tableau Algorithm for the Guarded Fragment	145
	Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas	160
	Integration of Equality Reasoning into the Disconnection Calculus	176
	Analytic Sequent Calculi for Abelian and Lukasiewicz Logics	191
	Analytic Tableau Systems for Propositional Bimodal Logics of Knowledge and Belief	206
	A Confluent Theory Connection Calculus	221
	On Uniform Word Problems Involving Bridging Operators on Distributive Lattices	235
	Question Answering: From Partitions to Prolog	251
	A General Theorem Prover for Quantified Modal Logics	266
	Some New Exceptions for the Semantic Tableaux Version of the Second Incompleteness Theorem	281
	A New Indefinite Semantics for Hilbert's Epsilon	298
	A Tableau Calculus for Combining Non-disjoint Theories	315
	LINK: A Proof Environment Based on Proof Nets	330
	DCTP 1.2 - System Abstract	335
	Author Index	341