Automated deduction – CADE-14. 14th international conference on automated deduction, Townsville, North Queensland, Australia. July 13–17, 1997. Proceedings. (English) Zbl 1415.68038

Lecture Notes in Computer Science 1249. Lecture Notes in Artificial Intelligence. Berlin: Springer (ISBN 978-3-540-63104-0/pbk; 978-3-540-69140-2/ebook). xiv, 462 p. (1997).

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]


68-06 Proceedings, conferences, collections, etc. pertaining to computer science
03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
00B25 Proceedings of conferences of miscellaneous specific interest


Zbl 1102.68317
Full Text: DOI