LPAR-26: THE 26TH CONFERENCE ON LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING

A
Artikis, Alexander	Stream Reasoning with Sequencing
B
Baaz, Matthias	First-Order Tableaux with Unification for Henkin Quantifiers Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
Bartocci, Ezio	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
Blanqui, Frédéric	Aligning HOL-Light and Rocq libraries formally Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Bombardelli, Alberto	Induction and K-Induction for Hyperproperties
Briefs, Yasmine	Extending SMT Solving with Non-Ground Clause Learning
C
Cailler, Julie	Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB
Carelli, Mishel	Cycle Detection for Affine Integer Linear Loops
Chew, Leroy	Reintroducing the Second Player in EPR
Chiari, Michele	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
Chvalovský, Karel	Neural Conjecturing for Saturation Theorem Provers (short) Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
Cipollina, Matteo	Formalized Hopfield Networks and Boltzmann Machines
Codish, Michael	Compact Partial Symmetry Breaking for Graph Search Problems
Corbineau, Pierre	A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions
D
Delorme, Noé	Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB
Dershowitz, Nachum	de Vrijer's Strong Normalization in Haskell
Dokoupil, David	Simple Complementation of Generalized Büchi Automata
F
Finkbeiner, Bernd	Cycle Detection for Affine Integer Linear Loops
Fiuk, Oskar	Pushing the Limits of Decidability: Maslov's class K with Equivalence
Foster, Nate	TBA
G
Gamsakhurdia, Mariami	First-Order Tableaux with Unification for Henkin Quantifiers Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
Gheorghiu, Alexander V.	Towards an Operational Proof-theoretic Semantics
Gontard, Antoine	Aligning HOL-Light and Rocq libraries formally
Gros, Basile	A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions
H
Henne, Michał	Subsumption in FL_⊥reg with TBox Is in ExpTime.
Henzinger, Thomas	Reasoning About Hyperproperties with Automated Theorem Provers
Heule, Marijn	Coloring Queens with Thousands of Encodings
Hithnawi, Anwar	Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
Huisman, Marieke	Bug-free embedded software: a realisable dream? (and how VerCors will help…)
J
Jakubův, Jan	Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA
Janota, Mikoláš	Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA Reintroducing the Second Player in EPR Compact Partial Symmetry Breaking for Graph Search Problems
K
Karatarakis, Michail	Formalized Hopfield Networks and Boltzmann Machines A Formalized Neurodynamic Solver for $N$-Queens Completion
Karthikeyan, Ashwin	Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
Kharitonov, Ethan	Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
Korovin, Konstantin	Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Kovács, Laura	Reasoning About Hyperproperties with Automated Theorem Provers Thousands of Problems to Lean Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Kupferman, Orna	Blinking Synthesis
L
Lammel, Florian	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
Leferink, Wouter	Tight Complexity for Modal Extensions of Lec with K, 4, T
Leuștean, Ioana	Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
Li, Ao	Formally Solving Answer-Construction Problems in Lean
Lolic, Anela	First-Order Tableaux with Unification for Henkin Quantifiers
M
Macovei, Bogdan	Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
Maddison, Chris	Formally Solving Answer-Construction Problems in Lean
Mahler, Stella	First-Order Tableaux with Unification for Henkin Quantifiers
Meel, Kuldeep	Formally Solving Answer-Construction Problems in Lean Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
Monin, Jean-Francois	A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions
Morawska, Barbara	Subsumption in FL_⊥reg with TBox Is in ExpTime.
N
Narodytska, Nina	Using Formal Verification for the Text-to-SQL Task
Nießen, Tobias	Reasoning About Hyperproperties with Automated Theorem Provers
O
Oliveira da Costa, Ana	Reasoning About Hyperproperties with Automated Theorem Provers
Olsak, Miroslav	Reintroducing the Second Player in EPR
Oltean, Andrei-Alexandru	Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
Ong, C.-H. Luke	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
P
Palmeri, Jordin	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
Panja, Promit	Comparison Invariants for Verifying Control Invariance
Parys, Paweł	Subsumption in FL_⊥reg with TBox Is in ExpTime.
Pitsikalis, Manolis	Stream Reasoning with Sequencing
Platzer, André	Comparison Invariants for Verifying Control Invariance
Polaczek, Axel	Thousands of Problems to Lean
Przybocki, Benjamin	Coloring Queens with Thousands of Encodings A SAT Attack on Tarski's High School Algebra Problem
R
Ramanayake, Revantha	Tight Complexity for Modal Extensions of Lec with K, 4, T
S
Sanchez, Cesar	Induction and K-Induction for Hyperproperties
Schoisswohl, Johannes	Reasoning About Hyperproperties with Automated Theorem Provers Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Schreuder, Anne	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
Schuckman, Jacob	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
Secrist, Liam	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
Shamash Halevy, Naama	Blinking Synthesis
Steen, Alexander	Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic Experiments on Automating Boolos Curious Inference
Strejček, Jan	Simple Complementation of Generalized Büchi Automata
Stuckey, Peter	Compact Partial Symmetry Breaking for Graph Search Problems
Subercaseaux, Bernardo	Coloring Queens with Thousands of Encodings A SAT Attack on Tarski's High School Algebra Problem
Suda, Martin	Reintroducing the Second Player in EPR Neural Conjecturing for Saturation Theorem Provers (short) Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
Sun, Jialiang	Formally Solving Answer-Construction Problems in Lean
T
Tammet, Tanel	Knowledge Representation and Proof Search for English-to-Logic Question Answering
Tang, Yuzhi	Formally Solving Answer-Construction Problems in Lean
Taprogge, Melanie	Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic Experiments on Automating Boolos Curious Inference
Tinelli, Cesare	TBA
Tonetta, Stefano	Induction and K-Induction for Hyperproperties
Tourret, Sophie	Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB
Truong, Ha	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
U
Urban, Josef	Neural Conjecturing for Saturation Theorem Provers (short) Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
V
Viswanathan, Arjun	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
Voronkov, Andrei	Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
W
Weidenbach, Christoph	Extending SMT Solving with Non-Ground Clause Learning
Wiedijk, Freek	Formalized Hopfield Networks and Boltzmann Machines
Winkler, Lorenz	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
Z
Zamponi, Marco	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
Zohar, Yoni	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq

Disclaimer | Powered by EasyChair Smart Program