Volume
@proceedings{LPAR-26,
title = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
year = {2026}}
Papers
@inproceedings{LPAR-26:Formally_Solving_Answer_Construction,
author = {Jialiang Sun and Yuzhi Tang and Ao Li and Chris Maddison and Kuldeep S. Meel},
title = {Formally Solving Answer-Construction Problems in Lean},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/NnrB},
doi = {10.29007/s4zb},
pages = {1-21},
year = {2026}}
@inproceedings{LPAR-26:Aligning_HOL_Light_Rocq,
author = {Frédéric Blanqui and Antoine Gontard},
title = {Aligning HOL-Light and Rocq Libraries Formally},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/RZx3},
doi = {10.29007/cc85},
pages = {22-41},
year = {2026}}
@inproceedings{LPAR-26:Teaching_Vampire_New_Tricks,
author = {Karel Chvalovský and Martin Suda and Josef Urban},
title = {Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/vLFt},
doi = {10.29007/9dkc},
pages = {42-60},
year = {2026}}
@inproceedings{LPAR-26:Reintroducing_Second_Player_EPR,
author = {Leroy Chew and Mikoláš Janota and Miroslav Olšák and Martin Suda},
title = {Reintroducing the Second Player in EPR},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/4vvj},
doi = {10.29007/sfg8},
pages = {61-79},
year = {2026}}
@inproceedings{LPAR-26:LLM_Assisted_Formal_Verification,
author = {Ha Truong and Jordin Palmeri and Liam Secrist and Jacob Schuckman and Arjun Viswanathan and Yoni Zohar},
title = {LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/MjQR},
doi = {10.29007/xtl7},
pages = {80-90},
year = {2026}}
@inproceedings{LPAR-26:Stream_Reasoning_with_Sequencing,
author = {Manolis Pitsikalis and Alexander Artikis},
title = {Stream Reasoning with Sequencing},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/lH4k},
doi = {10.29007/j49q},
pages = {91-108},
year = {2026}}
@inproceedings{LPAR-26:Challenging_Benchmarks_Diagrammatic_Equivalence,
author = {Julie Cailler and Noé Delorme and Sophie Tourret},
title = {Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/vwkf},
doi = {10.29007/72rt},
pages = {109-126},
year = {2026}}
@inproceedings{LPAR-26:Induction_K_Induction_Hyperproperties,
author = {Alberto Bombardelli and Cesar Sanchez and Stefano Tonetta},
title = {Induction and K-Induction for Hyperproperties},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/rSrc},
doi = {10.29007/s7mw},
pages = {127-145},
year = {2026}}
@inproceedings{LPAR-26:STLSat_—_Improved_Tableau,
author = {Marco Zamponi and Florian Lammel and Ezio Bartocci and Michele Chiari},
title = {STLSat — An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/hKhT},
doi = {10.29007/dhgk},
pages = {146-166},
year = {2026}}
@inproceedings{LPAR-26:Enhancing_Superposition_Reasoning_Linear,
author = {Johannes Schoisswohl and Laura Kovács and Konstantin Korovin and Andrei Voronkov},
title = {Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/TCsRH},
doi = {10.29007/9sfw},
pages = {167-186},
year = {2026}}
@inproceedings{LPAR-26:Reasoning_About_Hyperproperties_with,
author = {Tobias Nießen and Ana Oliveira da Costa and Johannes Schoisswohl and Thomas A. Henzinger and Laura Kovács},
title = {Reasoning About Hyperproperties with Automated Theorem Provers},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/HpdN},
doi = {10.29007/9lfj},
pages = {187-199},
year = {2026}}
@inproceedings{LPAR-26:Subsumption_FL_⊥reg_with_TBox,
author = {Michał Henne and Barbara Morawska and Paweł Parys},
title = {Subsumption in FL_⊥reg with TBox Is in ExpTime.},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/hZSd},
doi = {10.29007/flpw},
pages = {200-216},
year = {2026}}
@inproceedings{LPAR-26:Formal_Verification_Proofs_from,
author = {Melanie Taprogge and Frédéric Blanqui and Alexander Steen},
title = {Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/vTck},
doi = {10.29007/brmk},
pages = {217-237},
year = {2026}}
@inproceedings{LPAR-26:Thousands_Problems_Lean,
author = {Laura Kovács and Axel Polaczek},
title = {Thousands of Problems to Lean},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/lRS7},
doi = {10.29007/9kg5},
pages = {238-249},
year = {2026}}
@inproceedings{LPAR-26:Formalized_Hopfield_Networks_Boltzmann,
author = {Matteo Cipollina and Michail Karatarakis and Freek Wiedijk},
title = {Formalized Hopfield Networks and Boltzmann Machines},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/DTg2},
doi = {10.29007/25fj},
pages = {250-270},
year = {2026}}
@inproceedings{LPAR-26:Minimalist_Approach_Trustworthy_Programming,
author = {Pierre Corbineau and Basile Gros and Jean-Francois Monin},
title = {A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/xHSb5},
doi = {10.29007/7bjb},
pages = {271-289},
year = {2026}}
@inproceedings{LPAR-26:Scaling_Zero_Knowledge_UNSAT,
author = {Ashwin Karthikeyan and Ethan Kharitonov and Kuldeep S. Meel and Anwar Hithnawi},
title = {Scaling Zero Knowledge UNSAT Verification via Normalized Chaining},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/F5NK},
doi = {10.29007/g7v2},
pages = {290-308},
year = {2026}}
@inproceedings{LPAR-26:Extending_SMT_Solving_with,
author = {Yasmine Briefs and Christoph Weidenbach},
title = {Extending SMT Solving with Non-Ground Clause Learning},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/vXQW},
doi = {10.29007/x89r},
pages = {309-329},
year = {2026}}
@inproceedings{LPAR-26:Blinking_Synthesis,
author = {Orna Kupferman and Naama Shamash Halevy},
title = {Blinking Synthesis},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/s6TF},
doi = {10.29007/15vc},
pages = {330-347},
year = {2026}}
@inproceedings{LPAR-26:First_Order_Tableaux_with,
author = {Matthias Baaz and Mariami Gamsakhurdia and Anela Lolic and Stella Mahler},
title = {First-Order Tableaux with Unification for Henkin Quantifiers},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/3Vr3},
doi = {10.29007/hvv6},
pages = {348-363},
year = {2026}}
@inproceedings{LPAR-26:Tight_Complexity_Modal_Extensions,
author = {Wouter Leferink and Revantha Ramanayake},
title = {Tight Complexity for Modal Extensions of Lec with K, 4, T},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/hK2D},
doi = {10.29007/n4zl},
pages = {364-380},
year = {2026}}
@inproceedings{LPAR-26:Comparison_Invariants_Verifying_Control,
author = {Promit Panja and André Platzer},
title = {Comparison Invariants for Verifying Control Invariance},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/9ZkQ},
doi = {10.29007/5zft},
pages = {381-400},
year = {2026}}
@inproceedings{LPAR-26:Compact_Partial_Symmetry_Breaking,
author = {Michael Codish and Mikoláš Janota and Peter J. Stuckey},
title = {Compact Partial Symmetry Breaking for Graph Search Problems},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/zWKL},
doi = {10.29007/xvnx},
pages = {401-417},
year = {2026}}
@inproceedings{LPAR-26:de_Vrijers_Strong_Normalization,
author = {Nachum Dershowitz},
title = {de Vrijer's Strong Normalization in Haskell},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/lPRn},
doi = {10.29007/1flx},
pages = {418-429},
year = {2026}}
@inproceedings{LPAR-26:Maslovs_class_K_with,
author = {Oskar Fiuk},
title = {Maslov's class K with Equivalence},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/PGQ3},
doi = {10.29007/77xd},
pages = {430-448},
year = {2026}}
@inproceedings{LPAR-26:Coloring_Queens_with_Thousands,
author = {Bernardo Subercaseaux and Benjamin Przybocki and Marijn Heule},
title = {Coloring Queens with Thousands of Encodings},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/xnQT},
doi = {10.29007/rvv9},
pages = {449-464},
year = {2026}}
@inproceedings{LPAR-26:SAT_Attack_Tarskis_High,
author = {Bernardo Subercaseaux and Benjamin Przybocki},
title = {A SAT Attack on Tarski's High School Algebra Problem},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/Z28t},
doi = {10.29007/8l4s},
pages = {465-484},
year = {2026}}
@inproceedings{LPAR-26:Polynomial_Invariants_Probabilistic_Transition,
author = {Anne Schreuder and Lorenz Winkler and Laura Kovács and C.-H. Luke Ong},
title = {Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/vJkd},
doi = {10.29007/7hmx},
pages = {485-503},
year = {2026}}
@inproceedings{LPAR-26:Simple_Complementation_Generalized_Büchi,
author = {David Dokoupil and Jan Strejček},
title = {Simple Complementation of Generalized Büchi Automata},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/zjrt},
doi = {10.29007/hngx},
pages = {504-524},
year = {2026}}
@inproceedings{LPAR-26:Experiments_Automating_Boolos_Curious,
author = {Alexander Steen and Melanie Taprogge},
title = {Experiments on Automating Boolos' Curious Inference},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/Njnd},
doi = {10.29007/rbsg},
pages = {525-534},
year = {2026}}
@inproceedings{LPAR-26:Representation_Abstraction_Proof_Search,
author = {Tanel Tammet},
title = {Representation Abstraction and Proof Search for English-to-Logic Question Answering},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/F4bW},
doi = {10.29007/m947},
pages = {535-547},
year = {2026}}
@inproceedings{LPAR-26:Formalizing_Many_Sorted_Hybrid,
author = {Alexandru Oltean and Bogdan Macovei and Ioana Leuștean},
title = {Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean},
booktitle = {Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
editor = {Erika Ábrahám and Nikolaj Bjørner and Michael Rawson},
series = {EPiC Series in Computing},
volume = {112},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/GnVW},
doi = {10.29007/w6q5},
pages = {548-565},
year = {2026}}
