Volume 162,
Numbers 1-2,
October/November 2000
- John K. Slaney:
Introduction.
1-2 BibTeX
- Qing Guo, Paliath Narendran, David A. Wolfram:
Complexity of Nilpotent Unification and Matching Problems.
3-23 BibTeX
- Miki Hermann, Phokion G. Kolaitis:
Unification Algorithms Cannot Be Combined in Polynomial Time.
24-42 BibTeX
- Olivier Roussel, Philippe Mathieu:
The Achievement of Knowledge Bases by Cycle Search.
43-58 BibTeX
- Jörg Denzinger, Stephan Schulz:
Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts.
59-79 BibTeX
- David A. Basin, Seán Matthews:
Structuring Metatheory on Inductive Definitions.
80-95 BibTeX
- Christoph Walther, Thomas Kolbe:
On Terminating Lemma Speculations.
96-116 BibTeX
- Giuseppe De Giacomo, Fabio Massacci:
Combining Deduction and Model Checking into Tableaux and Algorithms for Converse-PDL.
117-137 BibTeX
- Heribert Schütz, Tim Geisler:
Efficient Model Generation through Compilation.
138-157 BibTeX
- Fausto Giunchiglia, Roberto Sebastiani:
Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m).
158-178 BibTeX
- Tai Joon Park, Allen Van Gelder:
Partitioning Methods for Satisfiability Testing on Large Formulas.
179-184 BibTeX
- Gernot Salzer:
Optimal Axiomatizations of Finitely Valued Logics.
185-205 BibTeX
- Saturnino F. Luz-Filho:
Using Tableaux to Automate the Lambek and Other Categorial Calculi.
206-225 BibTeX
- Christoph Kreitz, Stephan Schmitt:
A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems.
226-254 BibTeX
- Uwe Egly, Thomas Rath:
Practically Useful Variants of Definitional Translations to Normal Form.
255-264 BibTeX
Copyright © Sun May 17 00:00:00 2009
by Michael Ley (ley@uni-trier.de)
