This page lists citations (by people other than myself) of my
published works that I know about, it is probably incomplete. If
you happen to know other citations of my papers (e.g., because
you cited one), I would appreciate it if you would send me an
e-mail.
- On the
weakness of sharply bounded polynomial induction
- M. Tada and M. Tatsuta The function [a/m] in sharply
bounded arithmetic. Arch. Math. Logic 37 (1997)
- M. Tada Division in the theory
S02+ of Bounded Arithmetic.
Interdisciplinary Information Sciences 3 (1997)
- C. Pollett Multifunction algebras and the
provability of PH. Annals of Pure and Applied Logic
104 (2000)
- S. Kuroda An Independence Result on Weak Second
Order Bounded Arithmetic. Math. Logic Quarterly 47
(2001)
- C. Pollett On the Bounded Version of Hilbert's
Tenth Problem. Arch. Math. Logic 42 (2003)
- E. Jerábek The strength of sharply bounded
induction. Math. Logic Quarterly 52 (2006)
- A note on
sharply bounded arithmetic
- C. Pollett A propositional proof system for
Ri2. In: Proof Complexity and
Feasible Arithmetics, P. Beame and S. Buss (eds.), AMS
1998
- T. Arai Some results on cut-elimination, provable
well-orderings, induction and reflection Annals of
Pure and Applied Logic 95 (1998)
- A. Beckmann A note on universal measures for weak
implicit complexity. 9th International Conference
Logic for Programming, Artificial Intelligence, and
Reasoning (2002)
- A. Beckmann Dynamic ordinal analysis.
Arch. Math. Logic 42 (2003)
- A. Beckmann Generalised dynamic ordinals - universal
measures for implicit computational complexity.
Logic Colloquium '02, Lecture Notes in Logic 27, 2006
- E. Jerábek The strength of sharply bounded
induction. Math. Logic Quarterly 52 (2006)
- Schwache
Fragmente der Arithmetik und Schwellwertschaltkreise
beschränkter Tiefe
- P. Clote Computation models and function
algebras. In: Handbook of Computatbility Theory,
E. R. Griffor (ed.), Elsevier 1999
- T. Coquand and M. Hofmann A new method for
establishing conservativity of classical systems over
their intuitionistic version. Mathematical
Structures in Computer Science 9 (1999)
- P. Clote and E. Kranakis Boolean Functions and
Computation Models. Springer Texts in Theoretical
Computer Science 2002
- A bounded
arithmetic theory for constant depth threshold
circuits
- S. A. Cook and P. Nguyen VTC0: A
Second-Order Theory for TC0. 19th IEEE
Symposium on Logic in Computer Science (2004)
- P. Nguyen and S. A. Cook Theories for TC0 and other
Small Complexity Classes. Logical Methods in
Computer Science Vol. 2 Issue 1 (2006)
- A. Cordon-Franco, A. Fernandez-Margarit and F. F. Lara-Martin
On rules and parameter-free systems in bounded arithmetic.
Computation and Logic in the Real World, CiE 2007
- F. Ferreira and G. Ferreira The Riemann integral in
weak systems of analysis. Journal of Universal
Computer Science 14, 2008
- A
model-theoretic property of sharply bounded formulae, with
some applications
- C. Pollett Multifunction algebras and the
provability of PH. Annals of Pure and Applied Logic
104 (2000).
- S. Kuroda An independence result on weak second
order Bounded Arithmetic. Math. Logic Quarterly 47
(2001)
- M. Moniri Comparing constructive arithmetical
theories based on NP-PIND and coNP-PIND. J. Logic
Computat. 13 No. 6 (2003)
- C. Pollett On the Bounded Version of Hilbert's
Tenth Problem. Arch. Math. Logic 42 (2003)
- M. Moniri Model Theory of Bounded Arithmetic With
Applications to Independence Results. In
Logic in Tehran, Lecture Notes in Logic
26 (2006)
- M. Moniri An independence result for intuitionistic
Bounded Arithmetic. J. Logic
Computat. 16 No. 2 (2006)
- E. Jerábek The strength of sharply bounded
induction. Math. Logic Quarterly 52 (2006)
- Lower bounds
for monotone real circuit depth and formula size and
tree-like cutting planes
- P. Pudlák The lengths of proofs. In: Handbook of
Proof Theory, S.R. Buss (ed.), Elsevier 1998
- P. Clote and E. Kranakis Boolean Functions and
Computation Models. Springer Texts in Theoretical
Computer Science 2002
- On proofs
about threshold circuits and counting hierarchies
- S. A. Cook and P. Nguyen VTC0: A
Second-Order Theory for TC0. 19th IEEE
Symposium on Logic in Computer Science (2004)
- P. Nguyen and S. A. Cook Theories for TC0 and other
Small Complexity Classes. Logical Methods in
Computer Science Vol. 2 Issue 1 (2006)
- F. Ferreira, G.Ferreira Counting as integration in
feasible analysis Math. Logic Quarterly 52 (2006)
- S. A. Cook and N. Thapen The strength of replacement in
weak arithmetic. ACM Transactions on Computational
Logic 7 (2006)
- A. Cordon-Franco, A. Fernandez-Margarit and F. F. Lara-Martin
On rules and parameter-free systems in bounded arithmetic.
Computation and Logic in the Real World, CiE 2007
- F. Ferreira and G. Ferreira The Riemann integral in
weak systems of analysis. Journal of Universal
Computer Science 14, 2008
- Equational
calculi and constant-depth propositional proofs
- S. A. Cook and P. Nguyen VTC0: A
Second-Order Theory for TC0. 19th IEEE
Symposium on Logic in Computer Science (2004)
- P. Nguyen and S. A. Cook Theories for TC0 and other
Small Complexity Classes. Logical Methods in
Computer Science Vol. 2 Issue 1 (2006)
- A remark on
independence results for sharply bounded
arithmetic
- S. Kuroda An Independence Result on Weak Second
Order Bounded Arithmetic. Math. Logic Quarterly 47
(2001)
- M. Moniri Comparing constructive arithmetical
theories based on NP-PIND and coNP-PIND. J. Logic
Computat. 13 No. 6 (2003)
- M. Moniri Model Theory of Bounded Arithmetic With
Applications to Independence Results. In
Logic in Tehran, Lecture Notes in Logic
26 (2006)
- Exponential
separations between restricted resolution and
cutting planes proof systems
- K. Iwama and S. Miyazaki Tree-like Resolution is
superpolynomially slower than DAG-like Resolution for
the Pigeonhole Principle. 10th International
Symposium on Algorithms and Computation 1999
- M.L. Bonet and N. Galesi A Study of Proof Search
Algorithms for Resolution and Polynomial Calculus.
40th IEEE Symposium on Foundations of Computer Science
1999
- O. Kullmann Investigating a general hierarchy of
polynomially decidable classes of CNF~s based on short
tree-like resolution proofs. Electronic Colloquium
on Computational Complexity TR99-041, 1999
- N. H. Arai Relative Efficiency of Propositional
Proof Systems: Resolution vs. Cut-Free LK. Annals
of Pure and Applied Logic 104 (2000)
- J. Buresh-Oppenheim, M. Clegg, R. Impagliazzo and
T. Pitassi Homogenization and the Polynomial
Calculus. 27th International Colloquium on
Automata, Languages and Programming (2000)
- J. Messner On the Simulation Order of Proof
Systems. Dissertation, Universität Ulm, 2000
- S. Dash On the Matrix Cuts of Lovasz and Schrijver
and their use in Integer Programming. PhD Thesis,
Rice University, 2001
- J. Nordström Stalmarck's Method versus
Resolution: A Comparative Theoretical Study
Master's Thesis, KTH Stockholm, 2001
- K. Iwama and S. Yamashita A complete set of
transformation rules for quantum Boolean circuits with
CNOT gates. Superlattices and Microstructures 31 (2002)
- P. Clote and E. Kranakis Boolean Functions and
Computation Models. Springer Texts in Theoretical
Computer Science 2002
- E. Ben-Sasson Size Space Tradeoffs for
Resolution. ACM Symposium on Theory of Computing
2002
- E. Goldberg Proving Unsatisfiability of CNFs
Locally. Journal of Automated Reasoning 28 (2002)
- F. Bacchus, S. Dalmao and T. Pitassi Value
Elimination: Bayesian Interence via Backtracking
Search. 19th Conference in Uncertainty in
Artificial Intelligence (2003)
- K. Iwama and S. Yamashita Transformation rules for
CNOT-based quantum circuits and their applications.
New Generation Computing 21 (2003)
- F. Bacchus, S. Dalmao and T. Pitassi Algorithms and
Complexity Results for #SAT and Bayesian Inference.
44th Symposium on Foundations of Computer Science
(2003)
- J. Hwang A Theoretical Comparison of Resolution
Proof Systems for CSP Algorithms. MSc Thesis, Simon
Fraser University, 2004
- E. Ben-Sasson, R. Impagliazzo and A. Wigderson
Near-Optimal Separation of General and Tree-Like
Resolution. Combinatorica 24 (2004)
- J. Hwang and D. Mitchell 2-way vs d-way Branching
for CSP. 11th International Conference on Principles and Practice of
Constraint Programming, CP 2005
- Weak bounded
arithmetic, the Diffie-Hellman problem, and
Constable's class K
- C. Pollett and R. Pruim Strengths and Weaknesses of
LH Arithmetic. Math. Logic Quarterly 48 (2002)
- W. Hesse, E. Allender, D. A. Mix Barrington Uniform
constant-depth threshold circuits for division and
iterated multiplication. J. Comput. Syst. Sci. 65
(2002)
- On the
Δb1-bit-comprehension
rule
- C. Pollett A Theory for Logspace and NLIN versus
co-NLIN. Journal of Symbolic Logic 68 (2003)
- S. A. Cook and P. Nguyen VTC0: A
Second-Order Theory for TC0. 19th IEEE
Symposium on Logic in Computer Science (2004)
- S. A. Cook Theories for Complexity Classes and
their Propositional Translations. In: Complexity
of computations and proofs, Jan Krajicek (ed.), Quaderni
di Matematica (2005)
- P. Nguyen and S. A. Cook Theories for TC0 and other
Small Complexity Classes. Logical Methods in
Computer Science Vol. 2 Issue 1 (2006)
- S. A. Cook and N. Thapen The strength of replacement in
weak arithmetic. ACM Transactions on Computational
Logic 7 (2006)
- A. Cordon-Franco, A. Fernandez-Margarit and F. F. Lara-Martin
On rules and parameter-free systems in bounded arithmetic.
Computation and Logic in the Real World, CiE 2007
- On the
relative complexity of resolution refinements and cutting
planes proof systems
- E. Ben-Sasson and A. Wigderson Short Proofs are
Narrow - Resolution made Simple. Journal of the ACM
48 (2001)
- M. L. Bonet and N. Galesi Optimality of Size-width
Tradeoffs for Resolution. Computational Complexity
10 (2001)
- J. L. Esteban, J. Torán A combinatorial
characterization of treelike resolution space.
Inf. Process. Lett. 87 (2003)
- A. Sabharwal, P. Beame, H. Kautz Using Problem
Structure for Efficient Clause Learning. 6th
International Conference on Theory and Applications of
Satisfiability Testing 2003
- J. Buresh-Oppenheim, T. Pitassi The Complexity of
Resolution Refinements. 18th IEEE Symposium on Logic in
Computer Science 2003
- P. Beame, H. Kautz, A. Sabharwal Understanding the
Power of Clause Learning. 18th International Joint
Conference on Artificial Intelligence 2003
- P. Beame, R. Impagliazzo, T. Pitassi and N. Segerlind
Memoization and DPLL: Formula Caching Proof
Systems. IEEE Conference on Computational
Complexity 2003
- H. Kautz and B. Selman Ten Challenges Redux: Recent
Progress in Propositional Reasoning and Search.
9th International Conference on Principles and Practice of
Constraint Programming (2003)
- A. Atserias and M. L. Bonet On the Automatizability
of Resolution and Related Propositional Proof Systems.
Information and Computation 189 (2004)
- J. Torán Space and Width in Propositional
Resolution. EATCS Bulletin (2004)
- P. Beame, H. Kautz, A. Sabharwal Towards
understanding and harnessing the potential of clause
learning. Journal of Artificial Intelligence
Research 22 (2004)
- J. L. Esteban, N. Galesi, J. Messner On the
complexity of resolution with bounded conjunctions.
Theoretical Computer Science 321 (2004)
- R. Nieuwenhuis and A. Oliveras
Decision procedures for SAT, SAT Modulo Theories and
Beyond - The BarcelogicTools.
12th International Conference on Logic for Programming,
Artificial Intelligence and Reasoning, 2005.
- P. Liberatore Complexity results on DPLL and
Resolution. ACM Transactions on Computational
Logic 7 (2006)
- J. Nordström Narrow Proofs May Be Spacious:
Separating Space and Width in Resolution
ACM Symposium on Theory of Computing
2006
- R Nieuwenhuis, A Oliveras and C Tinelli
Solving SAT and SAT Modulo Theories: From an abstract
Davis--Putnam--Logemann--Loveland procedure to
DPLL(T). Journal of the ACM 53 (2006)
- J. Hoffmann, C. Gomes, B. Selman Structure and
problem hardness: goal asymmetry and DPLL proofs in
SAT-based planning Logical Methods in Computer
Science 3 (2007)
- A. Atserias, M. L. Bonet and J. Levy On Chvátal rank
and cutting planes proofs.
Theoretical Computer Science (to appear)
- H. Kautz and B. Selman The State of SAT.
Discrete Applied Mathematics (to appear)
- J. Nordström and J. Hastad Towards an Optimal
Separation of Space and Length in Resolution, ECCC
TR 08-026, 2008
- S.R. Buss and J.Hoffmann The NP-hardness of finding
a directed acyclic graph for regular resolution.
Theoretical Compter Science 396 (2008)
- Linear ramified higher type recursion and parallel complexity
- I. Oitavem Characterizing NC with tier 0 pointers.
Math. Logic Quarterly 50 (2003)
- U. Dal Lago The Geometry of Linear Higher-order Recursion. 20th IEEE Symposium on Logic in
Computer Science 2005
- G. Bonfante, R. Kahle, J.-Y. Marion and I. Oitavem
Towards an Implicit Characterization of
NCk.
Computer Science LOgic, 2006
- An exponential
separation between regular and general
resolution
- E. Ben-Sasson Size Space Tradeoffs for
Resolution. ACM Symposium on Theory of Computing
2002
- J. Buresh-Oppenheim, T. Pitassi The Complexity of
Resolution Refinements. 18th IEEE Symposium on Logic in
Computer Science 2003
- P. Beame, H. Kautz, A. Sabharwal Understanding the
Power of Clause Learning. 18th International Joint
Conference on Artificial Intelligence 2003
- J. Hwang A Theoretical Comparison of Resolution
Proof Systems for CSP Algorithms. MSc Thesis, Simon
Fraser University, 2004
- P. Beame, H. Kautz, A. Sabharwal Towards
understanding and harnessing the potential of clause
learning. Journal of Artificial Intelligence
Research 22 (2004)
- A. Van Gelder Input Distance and Lower Bounds for
Propositional Resolution Proof Length.
8th International Conference on Theory and Applications of
Satisfiability Testing 2005
- A. Van Gelder Pool Resolution and Its Relation to
Regular Resolution and DPLL with Clause Learning.
Logic for Programming, Artificial Intelligence, and
Reasoning, LPAR 2005
- J. Nordström Narrow Proofs May Be Spacious:
Separating Space and Width in Resolution. ACM Symposium on Theory of Computing
2006
- A. Urquhart Regular vs. General Resolution: an
improved separation, Proceedings of SAT 2008
- J. Nordström and J. Hastad Towards an Optimal
Separation of Space and Length in Resolution, ECCC
TR 08-026, 2008
- S.R. Buss and J.Hoffmann The NP-hardness of finding
a directed acyclic graph for regular resolution.
Theoretical Compter Science 396 (2008)
- CTL+ is complete for double
exponential time
- M. Lange A Lower Complexity Bound for Propositional
Dynamic Logic with Intersection. Advances in Modal
Logic Vol. 5, 2005
- A. Rabinovich, Ph. Schnoebelen BTL2 and the
expressive power of ECTL+. Information and
Computation (to appear)
- M. Lange and C. Lutz 2-ExpTime lower bounds for
Propositional Dynamic Logics with intersection.
The Journal of Symbolic Logic 70 (2005)
- Satisfiability
problems complete for deterministic logarithmic
space
- S. Perron A Propositional Proof System for Log
Space. 14th Annual Conference of the European
Association for Computer Science Logic, 2005
- Bounded
Arithmetic and Resolution-Based Proof Systems
- A. Beckmann Uniform proof complexity. Journal of
Logic and Computation 15 (2005)
- An elementary fragment of second-order lambda calculus
- K. Aehlig Induction and Inductive Definitions in
Fragments of Second-Order Arithmetic. The Journal of
Symbolic Logic 70 (2005)
- K.-H. Niggl and H. Wunderlich Certifying polynomial
time and linear/polynomial space for imperative
programs. SIAM Journal on Computing 35 (2006)
- Bounded model checking for all regular properties
- K. Heljanko, T. Junttila, M. Keinänen, M. Lange,
T. Latvala Bounded Model Checking for Weak Alternating
Büchi Automata. 18th International Conference
on Computer Aided Verification, 2006
- R. Bloem, A. Cimatti, I. Pill, M. Roveri and
S. Semprini Symbolic Implementation of Alternating
Automata.
11th International Conference on Implementation and Application
of Automata, 2006
- R. Oshman and O. Grumberg A New Approach to Bounded Model
Checking for Branching Time Logics.
5th International Symposium on Automated Technology for
Verification and Analysis, 2007
- Optimal lower bounds on regular expression size using communication complexity
- H. Gruber and M. Holzer
Finite Automata, Digraph Connectivity, and Regular Expression Size,
35th International Colloquium on Automata, Languages and Programming, 2008
- W. Gelade
Succinctness of regular expressions with interleaving, intersection and counting,
33rd International Symposium on Mathematical Foundations of Computer Science, 2008
- H. Gruber and M. Holzer
Language Operations with Regular Expressions of Polynomial Size.,
10th International Workshop on Descriptional Complexity of Formal Systems, 2008
- H. Gruber and M. Holzer
Provably Shorter Regular Expressions from Deterministic Finite Automata.
12th International Conference on Developments in Language Theory, 2008