| no |
title |
author |
magazine |
year |
volume |
issue |
page(s) |
type |
| 1 |
A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems
|
Kreitz, Christoph
|
|
2000
|
162 |
1-2 |
p. 226-254
29 p.
|
article
|
| 2 |
Author Index for Volume 162
|
|
|
2000
|
162 |
1-2 |
p. 265-
1 p.
|
article
|
| 3 |
Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts
|
Denzinger, Jörg
|
|
2000
|
162 |
1-2 |
p. 59-79
21 p.
|
article
|
| 4 |
Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m)
|
Giunchiglia, Fausto
|
|
2000
|
162 |
1-2 |
p. 158-178
21 p.
|
article
|
| 5 |
Combining Deduction and Model Checking into Tableaux and Algorithms for Converse-PDL
|
De Giacomo, Giuseppe
|
|
2000
|
162 |
1-2 |
p. 117-137
21 p.
|
article
|
| 6 |
Complexity of Nilpotent Unification and Matching Problems
|
Guo, Qing
|
|
2000
|
162 |
1-2 |
p. 3-23
21 p.
|
article
|
| 7 |
Efficient Model Generation through Compilation
|
Schütz, Heribert
|
|
2000
|
162 |
1-2 |
p. 138-157
20 p.
|
article
|
| 8 |
INTRODUCTION
|
Slaney, John
|
|
2000
|
162 |
1-2 |
p. 1-2
2 p.
|
article
|
| 9 |
On Terminating Lemma Speculations
|
Walther, Christoph
|
|
2000
|
162 |
1-2 |
p. 96-116
21 p.
|
article
|
| 10 |
Optimal Axiomatizations of Finitely Valued Logics
|
Salzer, Gernot
|
|
2000
|
162 |
1-2 |
p. 185-205
21 p.
|
article
|
| 11 |
Papers to Appear in Forthcoming Issues
|
|
|
2000
|
162 |
1-2 |
p. 266-
1 p.
|
article
|
| 12 |
Partitioning Methods for Satisfiability Testing on Large Formulas
|
Park, Tai Joon
|
|
2000
|
162 |
1-2 |
p. 179-184
6 p.
|
article
|
| 13 |
Practically Useful Variants of Definitional Translations to Normal Form
|
Egly, Uwe
|
|
2000
|
162 |
1-2 |
p. 255-264
10 p.
|
article
|
| 14 |
Structuring Metatheory on Inductive Definitions
|
Basin, David
|
|
2000
|
162 |
1-2 |
p. 80-95
16 p.
|
article
|
| 15 |
The Achievement of Knowledge Bases by Cycle Search
|
Roussel, Olivier
|
|
2000
|
162 |
1-2 |
p. 43-58
16 p.
|
article
|
| 16 |
Unification Algorithms Cannot Be Combined in Polynomial Time
|
Hermann, Miki
|
|
2000
|
162 |
1-2 |
p. 24-42
19 p.
|
article
|
| 17 |
Using Tableaux to Automate the Lambek and Other Categorial Calculi
|
Luz, Saturnino F.
|
|
2000
|
162 |
1-2 |
p. 206-225
20 p.
|
article
|
Journal description