Published in: Dagstuhl Reports, Volume 12, Issue 1 (2022)
Albert Atserias, Christoph Berkholz, Kousha Etessami, and Joanna Ochremiak. Finite and Algorithmic Model Theory (Dagstuhl Seminar 22051). In Dagstuhl Reports, Volume 12, Issue 1, pp. 101-118, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@Article{atserias_et_al:DagRep.12.1.101, author = {Atserias, Albert and Berkholz, Christoph and Etessami, Kousha and Ochremiak, Joanna}, title = {{Finite and Algorithmic Model Theory (Dagstuhl Seminar 22051)}}, pages = {101--118}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2022}, volume = {12}, number = {1}, editor = {Atserias, Albert and Berkholz, Christoph and Etessami, Kousha and Ochremiak, Joanna}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.1.101}, URN = {urn:nbn:de:0030-drops-169232}, doi = {10.4230/DagRep.12.1.101}, annote = {Keywords: automata and game theory, database theory, descriptive complexity, finite model theory, homomorphism counts, Query enumeration} }
Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
Ilario Bonacina, Nicola Galesi, and Massimo Lauria. On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 23:1-23:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{bonacina_et_al:LIPIcs.MFCS.2022.23, author = {Bonacina, Ilario and Galesi, Nicola and Lauria, Massimo}, title = {{On Vanishing Sums of Roots of Unity in Polynomial Calculus and Sum-Of-Squares}}, booktitle = {47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)}, pages = {23:1--23:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-256-3}, ISSN = {1868-8969}, year = {2022}, volume = {241}, editor = {Szeider, Stefan and Ganian, Robert and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.23}, URN = {urn:nbn:de:0030-drops-168211}, doi = {10.4230/LIPIcs.MFCS.2022.23}, annote = {Keywords: polynomial calculus, sum-of-squares, roots of unity, knapsack} }
Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
Dmitry Itsykson and Artur Riazanov. Automating OBDD proofs is NP-hard. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 59:1-59:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{itsykson_et_al:LIPIcs.MFCS.2022.59, author = {Itsykson, Dmitry and Riazanov, Artur}, title = {{Automating OBDD proofs is NP-hard}}, booktitle = {47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)}, pages = {59:1--59:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-256-3}, ISSN = {1868-8969}, year = {2022}, volume = {241}, editor = {Szeider, Stefan and Ganian, Robert and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.59}, URN = {urn:nbn:de:0030-drops-168575}, doi = {10.4230/LIPIcs.MFCS.2022.59}, annote = {Keywords: proof complexity, OBDD, automatability, lifting, dag-like communication} }
Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)
Albert Atserias. Towards a Theory of Algorithmic Proof Complexity (Invited Talk). In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 1:1-1:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{atserias:LIPIcs.ICALP.2022.1, author = {Atserias, Albert}, title = {{Towards a Theory of Algorithmic Proof Complexity}}, booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)}, pages = {1:1--1:2}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-235-8}, ISSN = {1868-8969}, year = {2022}, volume = {229}, editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.1}, URN = {urn:nbn:de:0030-drops-163423}, doi = {10.4230/LIPIcs.ICALP.2022.1}, annote = {Keywords: proof complexity, logic, computational complexity} }
Published in: LIPIcs, Volume 215, 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)
Anuj Dawar and Gregory Wilsenach. Lower Bounds for Symmetric Circuits for the Determinant. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 52:1-52:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{dawar_et_al:LIPIcs.ITCS.2022.52, author = {Dawar, Anuj and Wilsenach, Gregory}, title = {{Lower Bounds for Symmetric Circuits for the Determinant}}, booktitle = {13th Innovations in Theoretical Computer Science Conference (ITCS 2022)}, pages = {52:1--52:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-217-4}, ISSN = {1868-8969}, year = {2022}, volume = {215}, editor = {Braverman, Mark}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2022.52}, URN = {urn:nbn:de:0030-drops-156480}, doi = {10.4230/LIPIcs.ITCS.2022.52}, annote = {Keywords: arithmetic circuits, symmetric arithmetic circuits, Boolean circuits, symmetric circuits, permanent, determinant, counting width, Weisfeiler-Leman dimension, Cai-F\"{u}rer-Immerman constructions} }
Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)
Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the Power and Limitations of Branch and Cut. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 6:1-6:30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{fleming_et_al:LIPIcs.CCC.2021.6, author = {Fleming, Noah and G\"{o}\"{o}s, Mika and Impagliazzo, Russell and Pitassi, Toniann and Robere, Robert and Tan, Li-Yang and Wigderson, Avi}, title = {{On the Power and Limitations of Branch and Cut}}, booktitle = {36th Computational Complexity Conference (CCC 2021)}, pages = {6:1--6:30}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-193-1}, ISSN = {1868-8969}, year = {2021}, volume = {200}, editor = {Kabanets, Valentine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.6}, URN = {urn:nbn:de:0030-drops-142809}, doi = {10.4230/LIPIcs.CCC.2021.6}, annote = {Keywords: Proof Complexity, Integer Programming, Cutting Planes, Branch and Cut, Stabbing Planes} }
Published in: LIPIcs, Volume 200, 36th Computational Complexity Conference (CCC 2021)
Anastasia Sofronova and Dmitry Sokolov. Branching Programs with Bounded Repetitions and Flow Formulas. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 17:1-17:25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{sofronova_et_al:LIPIcs.CCC.2021.17, author = {Sofronova, Anastasia and Sokolov, Dmitry}, title = {{Branching Programs with Bounded Repetitions and Flow Formulas}}, booktitle = {36th Computational Complexity Conference (CCC 2021)}, pages = {17:1--17:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-193-1}, ISSN = {1868-8969}, year = {2021}, volume = {200}, editor = {Kabanets, Valentine}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2021.17}, URN = {urn:nbn:de:0030-drops-142915}, doi = {10.4230/LIPIcs.CCC.2021.17}, annote = {Keywords: proof complexity, branching programs, bounded repetitions, lower bounds} }
Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)
Albert Atserias. Proofs of Soundness and Proof Search (Invited Talk). In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, p. 2:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{atserias:LIPIcs.FSTTCS.2020.2, author = {Atserias, Albert}, title = {{Proofs of Soundness and Proof Search}}, booktitle = {40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-174-0}, ISSN = {1868-8969}, year = {2020}, volume = {182}, editor = {Saxena, Nitin and Simon, Sunil}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.2}, URN = {urn:nbn:de:0030-drops-132439}, doi = {10.4230/LIPIcs.FSTTCS.2020.2}, annote = {Keywords: Proof complexity, automatability, Resolution, proof search, consistency statements, lower bounds, reflection principle, satisfiability} }
Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)
Tuomas Hakoniemi. Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 63:1-63:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{hakoniemi:LIPIcs.ICALP.2020.63, author = {Hakoniemi, Tuomas}, title = {{Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares}}, booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)}, pages = {63:1--63:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-138-2}, ISSN = {1868-8969}, year = {2020}, volume = {168}, editor = {Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.63}, URN = {urn:nbn:de:0030-drops-124707}, doi = {10.4230/LIPIcs.ICALP.2020.63}, annote = {Keywords: Proof Complexity, Feasible Interpolation, Sums-of-Squares, Polynomial Calculus} }
Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)
Ana de Almeida Borges, Juan José Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten. The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 6:1-6:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{dealmeidaborges_et_al:LIPIcs.TIME.2019.6, author = {de Almeida Borges, Ana and Conejero Rodr{\'\i}guez, Juan Jos\'{e} and Fern\'{a}ndez-Duque, David and Gonz\'{a}lez Bedmar, Mireia and Joosten, Joost J.}, title = {{The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations}}, booktitle = {26th International Symposium on Temporal Representation and Reasoning (TIME 2019)}, pages = {6:1--6:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-127-6}, ISSN = {1868-8969}, year = {2019}, volume = {147}, editor = {Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.6}, URN = {urn:nbn:de:0030-drops-113649}, doi = {10.4230/LIPIcs.TIME.2019.6}, annote = {Keywords: linear temporal logic, monadic second order logic, formalized law, transport regulations} }
Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
Michal Garlík. Resolution Lower Bounds for Refutation Statements. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 37:1-37:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{garlik:LIPIcs.MFCS.2019.37, author = {Garl{\'\i}k, Michal}, title = {{Resolution Lower Bounds for Refutation Statements}}, booktitle = {44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)}, pages = {37:1--37:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-117-7}, ISSN = {1868-8969}, year = {2019}, volume = {138}, editor = {Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.37}, URN = {urn:nbn:de:0030-drops-109817}, doi = {10.4230/LIPIcs.MFCS.2019.37}, annote = {Keywords: reflection principles, refutation statements, Resolution, proof complexity} }
Published in: LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019)
Albert Atserias and Tuomas Hakoniemi. Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 24:1-24:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{atserias_et_al:LIPIcs.CCC.2019.24, author = {Atserias, Albert and Hakoniemi, Tuomas}, title = {{Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs}}, booktitle = {34th Computational Complexity Conference (CCC 2019)}, pages = {24:1--24:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-116-0}, ISSN = {1868-8969}, year = {2019}, volume = {137}, editor = {Shpilka, Amir}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.24}, URN = {urn:nbn:de:0030-drops-108464}, doi = {10.4230/LIPIcs.CCC.2019.24}, annote = {Keywords: Proof complexity, semialgebraic proof systems, Sums-of-Squares, Positivstellensatz, trade-offs, lower bounds, monomial size, degree} }
Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
Albert Atserias and Anuj Dawar. Definable Inapproximability: New Challenges for Duplicator. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 7:1-7:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{atserias_et_al:LIPIcs.CSL.2018.7, author = {Atserias, Albert and Dawar, Anuj}, title = {{Definable Inapproximability: New Challenges for Duplicator}}, booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)}, pages = {7:1--7:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-088-0}, ISSN = {1868-8969}, year = {2018}, volume = {119}, editor = {Ghica, Dan R. and Jung, Achim}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.7}, URN = {urn:nbn:de:0030-drops-96742}, doi = {10.4230/LIPIcs.CSL.2018.7}, annote = {Keywords: Descriptive Compleixty, Hardness of Approximation, MAX SAT, Vertex Cover, Fixed-point logic with counting} }
Published in: Dagstuhl Reports, Volume 8, Issue 1 (2018)
Albert Atserias, Jakob Nordström, Pavel Pudlák, and Rahul Santhanam. Proof Complexity (Dagstuhl Seminar 18051). In Dagstuhl Reports, Volume 8, Issue 1, pp. 124-157, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@Article{atserias_et_al:DagRep.8.1.124, author = {Atserias, Albert and Nordstr\"{o}m, Jakob and Pudl\'{a}k, Pavel and Santhanam, Rahul}, title = {{Proof Complexity (Dagstuhl Seminar 18051)}}, pages = {124--157}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2018}, volume = {8}, number = {1}, editor = {Atserias, Albert and Nordstr\"{o}m, Jakob and Pudl\'{a}k, Pavel and Santhanam, Rahul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.1.124}, URN = {urn:nbn:de:0030-drops-92864}, doi = {10.4230/DagRep.8.1.124}, annote = {Keywords: bounded arithmetic, computational complexity, logic, proof complexity, satisfiability algorithms} }
Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)
Albert Atserias, Stephan Kreutzer, and Marc Noy. On Zero-One and Convergence Laws for Graphs Embeddable on a Fixed Surface. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 116:1-116:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)
@InProceedings{atserias_et_al:LIPIcs.ICALP.2018.116, author = {Atserias, Albert and Kreutzer, Stephan and Noy, Marc}, title = {{On Zero-One and Convergence Laws for Graphs Embeddable on a Fixed Surface}}, booktitle = {45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)}, pages = {116:1--116:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-076-7}, ISSN = {1868-8969}, year = {2018}, volume = {107}, editor = {Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.116}, URN = {urn:nbn:de:0030-drops-91206}, doi = {10.4230/LIPIcs.ICALP.2018.116}, annote = {Keywords: topological graph theory, monadic second-order logic, random graphs, zero-one law, convergence law} }
Feedback for Dagstuhl Publishing