Show indexed articles as search result.

The articles of this volume will be reviewed individually For the preceding conference see [Zbl 1102.68317].
Indexed articles:
Wu, Wen-Tsün, The char-set method and its applications to automated reasoning, 1-3 [Zbl 1430.03041]
Durand, Irène; Middeldorp, Aart, Decidable call by need computations in term rewriting (extended abstract), 4-18 [Zbl 1430.68133]
Baader, Franz; Tinelli, Cesare, A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method, 19-33 [Zbl 1430.03036]
Niehren, Joachim; Pinkal, Manfred; Ruhrberg, Peter, On equality up-to constraints over finite trees, context unification, and one-step rewriting, 34-48 [Zbl 1430.68137]
Nieuwenhuis, Robert; Rivero, José Miguel; Vallejo, Miguel Angel, Dedam: a kernel of data structures and algorithms for automated deduction with equality clauses, 49-52 [Zbl 1430.68419]
Bonacina, Maria Paola, The clause-diffusion theorem prover Peers-mcd (system description), 53-56 [Zbl 1430.68394]
Dahn, B. I.; Gehne, J.; Honigmann, Th.; Wolf, A., Integration of automated and interactive theorem proving in ILF, 57-60 [Zbl 1430.68397]
Wolf, Andreas; Schumann, Johann, ILF-SETHEO: processing model elimination proofs for natural language output, 61-64 [Zbl 1430.68426]
Fischer, Bernd; Schumann, Johann M. Ph., SETHEO goes software engineering: application of ATP to software reuse, 65-68 [Zbl 1430.68404]
Yang, Lu; Fu, Hongguang; Zeng, Zhenbing, A practical symbolic algorithm for the inverse kinematics of 6R manipulators with simple geometry, 73-86 [Zbl 1430.70010]
Schumann, Johann, Automatic verification of cryptographic protocols with SETHEO, 87-100 [Zbl 1430.68422]
Bjørner, Nikolaj S.; Stickel, Mark E.; Uribe, Tomás E., A practical integration of first-order reasoning and decision procedures, 101-115 [Zbl 1430.03037]
Egly, Uwe, Some pitfalls of LK-to-LJ translations and how to avoid them, 116-130 [Zbl 1430.03071]
Korn, Daniel S.; Kreitz, Christoph, Deciding intuitionistic propositional logic via translation into classical logic, 131-145 [Zbl 1430.03039]
Iwanuma, Koji, Lemma matching for a PTTP-based top-down theorem prover, 146-160 [Zbl 1430.68413]
Roussel, Olivier; Mathieu, Philippe, Exact knowledge compilation in predicate calculus: the partial achievement case, 161-175 [Zbl 1430.68421]
Hasegawa, Ryuzo; Inoue, Katsumi; Ohta, Yoshihiko; Koshimura, Miyuki, Non-Horn magic sets to incorporate top-down inference into bottom-up theorem proving, 176-190 [Zbl 1430.68410]
Vardi, Moshe Y., Alternating automata: unifying truth and validity checking for temporal logics, 191-206 [Zbl 1430.68156]
Kreitz, C.; Mantel, H.; Otten, J.; Schmitt, S., Connection-based proof construction in linear logic, 207-221 [Zbl 1430.03040]
Harland, James; Pym, David, Resource-distribution via Boolean constraints (extended abstract), 222-236 [Zbl 1422.03129]
Cryan, Mary; Ramsay, Allan, Constructing a normal form for property theory, 237-251 [Zbl 1430.68396]
Benzmüller, Christoph; Cheikhrouhou, Lassaad; Fehrer, Detlef; Fiedler, Armin; Huang, Xiaorong; Kerber, Manfred; Kohlhase, Michael; Konrad, Karsten; Meier, Andreas; Melis, Erica; Schaarschmidt, Wolf; Siekmann, Jörg; Sorge, Volker, \(\Omega\)mega: towards a mathematical assistant, 252-255 [Zbl 1430.68393]
Kolbe, Thomas; Brauburger, Jürgen, Plagiator – a learning prover, 256-259 [Zbl 1430.68414]
Fuchs, Dirk; Fuchs, Matthias, CoDe: a powerful prover for problems of condensed detachment, 260-263 [Zbl 1430.68405]
Giunchiglia, Fausto; Roveri, Marco; Sebastiani, Roberto, A new method for testing decision procedures in modal logics, 264-267 [Zbl 1430.68409]
Slaney, John, Minlog: a minimal logic theorem prover, 268-271 [Zbl 1430.68424]
Zhang, Hantao, SATO: an efficient propositional prover, 272-275 [Zbl 1430.68427]
Dennis, Louise; Bundy, Alan; Green, Ian, Using a generalisation critic to find bisimulations for coinductive proofs, 276-290 [Zbl 1430.68399]
Hutter, Dieter; Kohlhase, Michael, A colored version of the \(\lambda\)-calculus, 291-305 [Zbl 1430.68412]
Matthews, Seán, A practical implementation of simple consequence relations using inductive definitions, 306-320 [Zbl 1430.68417]
Ganzinger, Harald; Meyer, Christoph; Weidenbach, Christoph, Soft typing for ordered resolution, 321-335 [Zbl 1430.68407]
de Nivelle, Hans, A classification of non-liftable orders for resolution, 336-350 [Zbl 1430.03038]
Felty, Amy P.; Howe, Douglas J., Hybrid interactive theorem proving using Nuprl and HOL, 351-365 [Zbl 1430.68403]
Eastaughffe, K. A.; Ozols, M. A.; Cant, A., Proof tactics for a theory of state machines in a graphical environment, 366-379 [Zbl 1430.68400]
von Oheimb, David; Gritzner, Thomas F., RALL: machine-supported proofs for relation algebra, 380-394 [Zbl 1430.68425]
Hickey, Jason J., Nuprl-Light: an implementation framework for higher-order logics, 395-399 [Zbl 1430.68411]
Bornat, Richard; Sufrin, Bernard, Jape: a calculator for animating proof-on-paper, 412-415 [Zbl 1430.68395]
Fuchs, Matthias, Evolving combinators, 416-430 [Zbl 1430.68406]
Défourneaux, Gilles; Peltier, Nicolas, Partial matching for analogy discovery in proofs and counter-examples, 431-445 [Zbl 1430.68398]
Ehrensberger, Jürgen; Zinn, Claus, DiaLog: a system for dialogue logic, 446-460 [Zbl 1430.68402]