Mechanizing Mathematical Reasoning Book

	A portrait of a scientist : logic, AI and politics	1
	Some reflections on proof transformations	14
	Rewrite and decision procedure laboratory : combining rewriting, satisfiability checking, and lemma speculation	30
	SAT-based decision procedures for automated reasoning : a unifying perspective	46
	Temporal dynamics of support and attack networks : from argumentation to zoology	59
	Footprints of conditionals	99
	Time for thinking big in AI	120
	Solving first-order constraints over the monadic class	132
	From MKRP to [Omega]MEGA	139
	Decidable variants of higher-order unification	154
	Normal natural deduction proofs (in non-classical logics)	169
	History and future of implicit and inductionless induction : beware the old Jade and the zombie!	192
	The flowering of automated reasoning	204
	Description logics as ontology languages for the semantic Web	228
	Living books, automated deduction and other strange things	249
	An essay on sabotage and obstruction	268
	Bridging theorem proving and mathematical knowledge retrieval	277
	Formal description of natural languages : an HPSG grammar of polish	297
	Psychological validity of schematic proofs	321
	Natural language proof explanation	342
	Why proof planning for maths education and how?	364
	Towards MultiMedia instruction in safe and secure systems	379
	The impact of models in software development	396
	Formal software development in MAYA	407
	A unification algorithm for analysis of protocols with blinded signatures	433
	Exploiting generic aspects of security models in formal developments	452
	Verification support environment	476
	SAT-based cooperative planning : a proposal	494
	Towards comprehensive computational models for plan-based control of autonomous robots	514
	Agents with exact foreknowledge	528
	Self-organisation in holonic multiagent systems	543