Logic for Programming, Artificial Intelligence, and Reasoning Book

	Independently checkable proofs from decision procedures : issues and progress	1
	Zap : automated theorem proving for software analysis	2
	Decision procedures for SAT, SAT modulo theories and beyond. The barcelogic tools	23
	Scaling up : computers vs. common sense	47
	A new constraint solver for 3D lattices and its application to the protein folding problem	48
	Disjunctive constraint lambda calculi	64
	Computational issues in exploiting dependent and-parallelism in logic programming : leftness detection in dynamic search trees	79
	The nomore++ approach to answer set solving	95
	Optimizing the runtime processing of types in polymorphic logic programming languages	110
	The four sons of Penrose	125
	An algorithmic account of Ehrenfeucht games on labeled successor structures	139
	Second-order principles in specification languages for object-oriented programs	154
	Strong normalization of the dual classical sequent calculus	169
	Termination of fair computations in term rewriting	184
	On confluence of infinitary combinatory reduction systems	199
	Matching with regular constraints	215
	Recursive path orderings can also be incremental	230
	Automating coherent logic	246
	The theorema environment for interactive proof development	261
	A first order extension of Stalmarck's method	276
	Regular derivations in basic superposition-based calculi	292
	On the finite satisfiability problem for the guarded fragment with transitivity	307
	Deciding separation logic formulae by SAT and incremental negative cycle elimination	322
	Monotone AC-tree automata	337
	On the specification of sequent systems	352
	Verifying and reflecting quantifier elimination for presburger arithmetic	367
	Integration of a software model checker into isabelle	381
	Experimental evaluation of classical automata constructions	396
	Automatic validation of transformation rules for Java verification against a rewriting semantics	412
	Reasoning about incompletely defined programs	427
	Model checking abstract state machines with answer set programming	443
	Characterizing provability in Bl's pointer logic through resource graphs	459
	A unified memory model for pointers	474
	Treewidth in verification : local vs. global	489
	Pushdown module checking	504
	Functional correctness proofs of encryption algorithms	519
	Towards automated proof support for probabilistic distributed systems	534
	Algebraic intruder deductions	549
	Satisfiability checking for PC(ID)	565
	Pool resolution and its relation to regular resolution and DPLL with clause learning	580
	Another complete local search method for SAT	595
	Inference from controversial arguments	606
	Programming cognitive agents in defeasible logic	621
	The relationship between reasoning about privacy and default logics	637
	Comparative similarity, tree automata, and diophantine equations	651
	Analytic tableaux for KLM preferential and cumulative logics	666
	Bounding resource consumption with godel-dummett logics	682
	On interpolation in existence logics	697
	Incremental integrity checking : limitations and possibilities	712
	Concepts of automata construction from LTL	728