Automated Deduction - CADE-14 Book

	The Char-Set Method and Its Applications to Automated Reasoning	1
	Decidable Call by Need Computations in Term Rewriting	4
	A New Approach for Combining Decision Procedures for the Word Problem, and Its Connection to the Nelson-Oppen Combination Method	19
	On Equality Up-to Constraints over Finite Trees, Context Unification, and One-Step Rewriting	34
	Dedam: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses	49
	The Clause-Diffusion Theorem Prover Peers-mcd	53
	Integration of Automated and Interactive Theorem Proving in ILF	57
	ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output	61
	SETHEO Goes Software Engineering: Application of ATP to Software Reuse	65
	Proving System Correctness with KIV 3.0	69
	A Practical Symbolic Algorithm for the Inverse Kinematics of 6R Manipulators with Simple Geometry	73
	Automatic Verification of Cryptographic Protocols with SETHEO	87
	A Practical Integration of First-Order Reasoning and Decision Procedures	101
	Some Pitfalls of LK-to-LJ Translations and How to Avoid Them	116
	Deciding Intuitionistic Propositional Logic via Translation into Classical Logic	131
	Lemma Matching for a PTTP-based Top-down Theorem Prover	146
	Exact Knowledge Compilation in Predicate Calculus: The Partial Achievement Case	161
	Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving	176
	Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics	191
	Connection-Based Proof Construction in Linear Logic	207
	Resource-Distribution via Boolean Constraints	222
	Constructing a Normal Form for Property Theory	237
	[Omega]MEGA: Towards a Mathematical Assistant	252
	PLAGIATOR: A Learning Prover	256
	CODE: A Powerful Prover for Problems of Condensed Detachment	260
	A New Method for Testing Decision Procedures in Modal Logics	264
	MINLOG: A Minimal Logic Theorem Prover	268
	SATO: An Efficient Propositional Prover	272
	Using a Generalisation Critic to Find Bisimulations for Coinductive Proofs	276
	A Colored Version of the [lambda]-Calculus	291
	A Practical Implementation of Simple Consequence Relations Using Inductive Definitions	306
	Soft Typing for Ordered Resolution	321
	A Classification of Non-Liftable Orders for Resolution	336
	Hybrid Interactive Theorem Proving Using Nuprl and HOL	351
	Proof Tactics for a Theory of State Machines in a Graphical Environment	366
	RALL: Machine-Supported Proofs for Relation Algebra	380
	Nuprl-Light: An Implementation Framework for Higher-Order Logics	395
	XIsabelle: A System Description	400
	XBarnacle: Making Theorem Provers More Accessible	404
	The Tableau Browser SNARKS	408
	Jape: A Calculator for Animating Proof-on-Paper	412
	Evolving Combinators	416
	Partial Matching for Analogy Discovery in Proofs and Counter-examples	431
	DIALOG: A System for Dialogue Logic	446
	Author Index	461