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