Compiled by Christine Houck - April 1998

M. Agrawal, E. Allender, R. Impagliazzo, T. Pitassi, S. Rudich. Reducing the complexity of Reductions.

M. Agrawal, E. Allender, S. Rudich. Reductions in Circuit Complexity: An Isomorphism Theorem and a Gap Theorem.

E. Allender and K.-J. Lange. RUSPACE(log n) is contained in DSPACE(log^2 n/loglog n).

E. Allender and K.-J. Lange. StUSPACE(log n) is contained in DSPACE(log^2 n/loglog n).

R. Alur and T.A. Henzinger. Modularity for times and hybrid systems.

R. Alur, K.L. McMillan, D.A. Peled. Model-checking of correctness conditions for concurrent objects.

P.W. Beame, S.R. Buss, eds.

S. Bloch. On parallel hierarchies and R^i_k.

M.P. Bonacina and J. Hsiang. On the modelling of search in theorem proving -- Towards a theory of strategy analysis. Technical Report, Department of Computer Science, The University of Iowa, December 1995.

M.P. Bonacina and J. Hsiang. On the representation of dynamic search spaces in theorem proving.

M.P. Bonacina and J. Hsiang. On the notion of complexity of search in theorem proving.

M.L. Bonet, C. Phillips, T. Warnow, S. Yooseph. Constructing Evolutionary Trees in the Presence of Polymorphic Characters.

M.L. Bonet, T. Pitassi, R. Raz. No Feasible Interpolation for TC^0-Frege Proofs.

R.B. Boppana and J.F. Lynch, eds.

K.B. Bruce, P.G. Kolaitis, D.M. Leivant, M.Y. Vardi. Panel - Logic in the computer science curriculum.

S.R. Buss.``Bounded arithmetic and propositional proof complexity.''

S.R. Buss.``Bounded arithmetic, cryptography and complexity.'' To appear in

S.R. Buss. ``Lower bounds on Nullstellensatz proofs via designs.''

S.R. Buss, R. Impagliazzo, J. Krajicek, P. Pudlak, A. Razborov, J. Sgall. ``Proof complexity in algebraic systems and constant depth Frege systems with modular counting.'' To appear in

S.R. Buss and T. Pitassi. ``Good degree bounds on Nullstellensatz refutations of the induction principle.'' To appear in

S.R. Buss and T. Pitassi. ``Resolution and the weak pigeonhole principle.'' To appear in

A. Carbone. A combinatorial theory of duplication and the structure of proofs. Submitted for publication, 1997

A. Carbone. Turning cycles into spirals.

A. Carbone and S. Semmes. Making Proofs without modus ponens: An introduction to the combinatorics and complexity of cut elimination.

A. Carbone and S. Semmes. Propositional Proofs via Combinatorial Geometry and the Search for Symmetry. IHES preprint M/96/, to appear in

G. Cherlin and B.J. Latka. A decision problem involving tournaments.

G. Cherlin and B.J. Latka. Forbidden subtournaments. Submitted to

A. Dawar, L. Hella, A. Seth. Ordering Finite Variable Types with Generalized Quantifiers, To appear in the

C. Daws, A. Olivero, S. Tripakis, S. Yovine. The tool KRONOS.

P.C. Eklof, B. Huisgen-Zimmermann, S. Shelah. Torsion modules, lattices and p-points.

K. Etessami, M.Y. Vardi, T. Wilke. First-order with two variables and unary temporal logic.

K. Etessami and T. Wilke. An Until Hierarchy for Temporal Logic.

J. Feigenbaum, S. Kannan, M.Y. Vardi, and M. Vishwanathan. Complexity of Problems on Graphs Represented as OBDDs.

E. Gradel, P.G. Kolaitis, M.Y. Vardi. On the Decision Problem for Two-Variable First-Order Logic.

M. Grohe. Equivalence in finite variable logics is complete for polynomial time.

R.H. Hardin, R.P. Kurshan, S.K. Shukla, M.Y. Vardi. A new heuristic for bad cycle detection using BDDs.

D. Harel, O. Kupferman, M.Y. Vardi. On the complexity of verifying concurrent transition systems.

N. Immerman. Special Year on Logic and Algorithms Tutorial Notes: Descriptive Complexity, DIMACS Tech Report 97-55, 1997

N. Immerman and P.G. Kolaitis, eds.

N. Immerman, M.Y. Vardi. Model checking and transitive-closure logic.

R. Jin and S. Shelah. Compactness of Loeb Spaces.

B.M. Kapron. Feasibly continuous type-two functionals. To appear in

P. Kolaitis. Special Year on Logic and Algorithms Tutorial Notes: Expressive Powers of Logics, DIMACS Tech Report 97-54, 1997

O. Kupferman, M.Y. Vardi. Module Checking. In

O. Kupferman, M.Y. Vardi. Module Checking Revisited.

O. Kupferman, M.Y. Vardi. Synthesis with incomplete information.

O. Kupferman, M.Y. Vardi. Verification of fair transition systems. In

O. Kupferman, M.Y. Vardi. Weal alternating automata are not that weak.

R. Kurshan and S. Shukla. Special Year on Logic and Algorithms Tutorial Notes: Complexity Issues in Automata-Theoretic Verification: The COSPAN Approach to Deal with These Issues, DIMACS Tech Report 97-57, 1997

B.J. Latka. A decidability result for quasi-orderings defined by obstructions. Submitted to

B.J. Latka. Session II.

B.J. Latka. Well-quasi-ordered classes of tournaments. To appear in

A. Lisitsa and V. Sazonov. Bounded Hyperset Theory and Web-like Data Bases.

A. Lisitsa and V. Sazonov. Delta-languages for sets and LOGSPACE computable graph transformers.

A. Lisitsa and V. Sazonov. On linear ordering of strongly extensional finitely-branching graphs and non-well-founded sets.

J.F. Lynch. Convergence Laws for Random Graphs, to appear in

J.F. Lynch. Pebble Games in Model Theory.

J.F. Lynch.

L. Pacholski, P. Krysta. The STO problem is NP-complete.

L. Pacholski, W. Szwast, L. Tendera. Complexity of Two-Variable Logic with Counting.

D. Peled, T. Wilke, and P. Wolper. An algorithmic approach for checking closure properties of omega-regular languages. In

D. Peled, T. Wilke, and P. Wolper. An algorithmic approach for checking closure properties of temporal logic specifications and omega-regular languages.

E. Rosen, S. Shelah, S. Weinstein. k-Universal finite graphs.

V. Sazonov and D. Sviridenko. Abstract deducibility and domain theory.

A. Seth. Implicit Definability vs. Weak Implicit Definability in Finite Model Theory, manuscript, 1996

A. Seth. A note on Ramified Version of McColm's Second Conjecture, manuscript, 1997 (to be revised)

A. Seth. Sharper Results on the Expressive Power of Generalized Quantifiers.

H. Schlingloff. Modelling Message Buffers with Binary Decision Diagrams.

H. Schlingloff. Verification of Finite-State Systems with Temporal Logic Model Checking. South African Computer Journal, 1997

A. Seth. Sharper results on the expressive power of generalized quantifiers. In

S. Shelah. Erdos and Renyi Conjecture.

J.H. Spencer, K. St. John. Random Sparse Bit Strings at the Threshold of Adjacency,

P.S. Thiagarajan and I. Walukiewicz. An expressively Complete Linear Time Temporal Logic. (LICS'97), 1997, pages 183-194

S. Tripakis and S. Yovine. Analysis of timed systems based on time-abstracting bisimulations.

M.Y. Vardi. Why is modal logic so robustly decidable? In

- Evaluation of the 1995-1996 Special Year on Logic and Algorithms prepared by Neil Immerman, chair (University of Massachusetts) and Tom Henzinger (UC - Berkeley) - October 1, 1996.

DIMACS home page

Contacting the Center

Last modified August 7, 1998