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

This page contains an index consisting of author-provided keywords.

A
Administrative	Opening
affine single-path linear-constrained loops	Cycle Detection for Affine Integer Linear Loops
alternations	Reintroducing the Second Player in EPR
autoformalization	Knowledge Representation and Proof Search for English-to-Logic Question Answering
automata theory	Blinking Synthesis
Automated Reasoning	Formally Solving Answer-Construction Problems in Lean Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification Thousands of Problems to Lean Towards an Operational Proof-theoretic Semantics
Automated Theorem Provers	Reasoning About Hyperproperties with Automated Theorem Provers
Automated Theorem Proving	Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic Knowledge Representation and Proof Search for English-to-Logic Question Answering Some Experiments with Twee-Style Goal-Directedness Benchmarking LLMs Against TPTP: A Vision for the Near Future
automation	Aligning HOL-Light and Rocq libraries formally
axiomatization	Comparison Invariants for Verifying Control Invariance
B
base-extension semantics	Towards an Operational Proof-theoretic Semantics
BCH codes	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
Benchmarking	Benchmarking LLMs Against TPTP: A Vision for the Near Future
Benchmarks	Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB Reasoning About Hyperproperties with Automated Theorem Provers
bitwise operations	An Implementation of Integer Presburger Arithmetic in a Math Education Tool
Boltzmann Machines	Formalized Hopfield Networks and Boltzmann Machines A Formalized Neurodynamic Solver for $N$-Queens Completion
Boolos Curious Inference	Experiments on Automating Boolos Curious Inference
branching vector addition systems	Tight Complexity for Modal Extensions of Lec with K, 4, T
C
calculus of inductive constructions	Aligning HOL-Light and Rocq libraries formally A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions
cardinality constraints	Coloring Queens with Thousands of Encodings
CDCL	Extending SMT Solving with Non-Ground Clause Learning
CEGAR	Compact Partial Symmetry Breaking for Graph Search Problems
certificates	Reasoning about Collections in SMT
Circuit equivalences	Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB
Claude Code	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
commonsense reasoning	Knowledge Representation and Proof Search for English-to-Logic Question Answering
comparison invariants	Comparison Invariants for Verifying Control Invariance
comparison systems	Comparison Invariants for Verifying Control Invariance
complementation	Simple Complementation of Generalized Büchi Automata
complexity	Cycle Detection for Affine Integer Linear Loops
Computational complexity	Subsumption in FL_⊥reg with TBox Is in ExpTime. Tight Complexity for Modal Extensions of Lec with K, 4, T
conjecturing	Neural Conjecturing for Saturation Theorem Provers (short)
control invariance	Comparison Invariants for Verifying Control Invariance
CUBO	A Formalized Neurodynamic Solver for $N$-Queens Completion
Cut-Introduction	Experiments on Automating Boolos Curious Inference
Cyber-Physical Systems	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
cycle detection	Cycle Detection for Affine Integer Linear Loops
D
databases	NetKAT: Learning Models and Solving Equations
de Vrijer's measure	de Vrijer's Strong Normalization in Haskell
Decidable fragments of first-order logic	Maslov's class K with Equivalence
defeasible reasoning	Knowledge Representation and Proof Search for English-to-Logic Question Answering
dependent types	A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions
Description Logics	Subsumption in FL_⊥reg with TBox Is in ExpTime.
differential dynamic logic	Comparison Invariants for Verifying Control Invariance
E
E-prover	Neural Conjecturing for Saturation Theorem Provers (short)
education tool	An Implementation of Integer Presburger Arithmetic in a Math Education Tool
Eigenvariable conditions	First-Order Tableaux with Unification for Henkin Quantifiers
embedded software	Bug-free embedded software: a realisable dream? (and how VerCors will help…)
English-to-logic translation	Knowledge Representation and Proof Search for English-to-Logic Question Answering
EPR	Reintroducing the Second Player in EPR
Epsilon calculus	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
equational theories	A SAT Attack on Tarski's High School Algebra Problem
Equivalence relations	Maslov's class K with Equivalence
Error correction	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
event calculus	Stream Reasoning with Sequencing
F
finite automata	An Implementation of Integer Presburger Arithmetic in a Math Education Tool
Finite model property	Maslov's class K with Equivalence
first-order logic	Efficient Linear Model Building and Clause Evaluation
First-Order Theorem Proving	Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
formal math	Formalized Hopfield Networks and Boltzmann Machines A Formalized Neurodynamic Solver for $N$-Queens Completion
Formal Methods	Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
formal verification	Using Formal Verification for the Text-to-SQL Task
G
generalized Büchi automata	Simple Complementation of Generalized Büchi Automata
goal-directed search	Some Experiments with Twee-Style Goal-Directedness
Google Gemini	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
graph coloring	Coloring Queens with Thousands of Encodings
graph symmetry	Compact Partial Symmetry Breaking for Graph Search Problems
greedy	Compact Partial Symmetry Breaking for Graph Search Problems
greedy runs	Simple Complementation of Generalized Büchi Automata
H
Hello	Opening
Henkin quantifiers	First-Order Tableaux with Unification for Henkin Quantifiers
Herbrand disjunctions	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
hereditary Harrop formulae	Towards an Operational Proof-theoretic Semantics
high school identities	A SAT Attack on Tarski's High School Algebra Problem
higher order logic	Building Blocks for Reasoning on the BEAM
Higher-Order Logic	Aligning HOL-Light and Rocq libraries formally Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic Experiments on Automating Boolos Curious Inference
Higher-order moments	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
Hopfield networks	Formalized Hopfield Networks and Boltzmann Machines A Formalized Neurodynamic Solver for $N$-Queens Completion
Hybrid Modal Logic	Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
HyperLTL	Induction and K-Induction for Hyperproperties
Hyperproperties	Reasoning About Hyperproperties with Automated Theorem Provers
I
imperfect information	Blinking Synthesis
Incomplete proofs	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
Incorrect proofs	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
induction	Induction and K-Induction for Hyperproperties
infinite-state systems	Tight Complexity for Modal Extensions of Lec with K, 4, T
integer presburger arithmetic	An Implementation of Integer Presburger Arithmetic in a Math Education Tool
Interactive Theorem Proving	Thousands of Problems to Lean Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
intuitionistic logic	Towards an Operational Proof-theoretic Semantics
Invariant synthesis	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
ITP Hammers	Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
IWIL	Building Blocks for Reasoning on the BEAM An Implementation of Integer Presburger Arithmetic in a Math Education Tool Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop Some Experiments with Twee-Style Goal-Directedness Efficient Linear Model Building and Clause Evaluation Benchmarking LLMs Against TPTP: A Vision for the Near Future Opening
K
k-induction	Induction and K-Induction for Hyperproperties
knowledge representation	Stream Reasoning with Sequencing Knowledge Representation and Proof Search for English-to-Logic Question Answering
L
Large Language Model	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
Large Language Models	Formally Solving Answer-Construction Problems in Lean Knowledge Representation and Proof Search for English-to-Logic Question Answering Benchmarking LLMs Against TPTP: A Vision for the Near Future
Lean 4	Formally Solving Answer-Construction Problems in Lean Formalized Hopfield Networks and Boltzmann Machines A Formalized Neurodynamic Solver for $N$-Queens Completion
Lean Prover	Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
lemma introduction	Neural Conjecturing for Saturation Theorem Provers (short)
library alignment	Aligning HOL-Light and Rocq libraries formally
Linear Arithmetic	Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Literal Selection	Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
LLM	Using Formal Verification for the Text-to-SQL Task
logic and types	Thousands of Problems to Lean
logic libraries	Building Blocks for Reasoning on the BEAM
logic programming	Towards an Operational Proof-theoretic Semantics
M
machine learning	Neural Conjecturing for Saturation Theorem Provers (short)
Many-Sorted Signatures	Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
Martingales	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
Maslov's class K	Maslov's class K with Equivalence
mathlib	Formalized Hopfield Networks and Boltzmann Machines A Formalized Neurodynamic Solver for $N$-Queens Completion
Mizar	Neural Conjecturing for Saturation Theorem Provers (short)
modal logics	Tight Complexity for Modal Extensions of Lec with K, 4, T
model building	Efficient Linear Model Building and Clause Evaluation
Model Checking	Induction and K-Induction for Hyperproperties Reasoning About Hyperproperties with Automated Theorem Provers Reasoning about Collections in SMT
multiplicative substructural logics	Tight Complexity for Modal Extensions of Lec with K, 4, T
N
natural language question answering	Knowledge Representation and Proof Search for English-to-Logic Question Answering
networking	NetKAT: Learning Models and Solving Equations
Neural Clause-Selection Guidance	Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
neural networks	Formalized Hopfield Networks and Boltzmann Machines A Formalized Neurodynamic Solver for $N$-Queens Completion
O
Opening	Opening
Optional stopping	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
P
parallelization	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
parameter tuning	Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA
pattern-matching	A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions
patterns	Compact Partial Symmetry Breaking for Graph Search Problems
permutation	Compact Partial Symmetry Breaking for Graph Search Problems
PhysLib	Formalized Hopfield Networks and Boltzmann Machines
Probabilistic programs	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
Program verification	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
programming languages	NetKAT: Learning Models and Solving Equations
Proof Checking	Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
Proof length	Experiments on Automating Boolos Curious Inference
Proof theory	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
Proof Verification	Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic Benchmarking LLMs Against TPTP: A Vision for the Near Future
proof-theoretic semantics	Towards an Operational Proof-theoretic Semantics
Proofs	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
Proofs of UNSAT	Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
Proving Strategies	Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
PSPACE	Reintroducing the Second Player in EPR
Pushdown games	Subsumption in FL_⊥reg with TBox Is in ExpTime.
Q
QBF	Reintroducing the Second Player in EPR
QF-LRA	Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA
queen's graph	Coloring Queens with Thousands of Encodings
R
Ramsey graphs	Compact Partial Symmetry Breaking for Graph Search Problems
reachability	Tight Complexity for Modal Extensions of Lec with K, 4, T
Real Arithmetic	Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Redundancy	Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Requirements Engineering	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
Rocq	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
Rocq Coq	A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions
S
SAT encodings	Coloring Queens with Thousands of Encodings
SAT solving	A SAT Attack on Tarski's High School Algebra Problem
Satisfiability	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
Satisfiability problem	Maslov's class K with Equivalence
saturation	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
Saturation-based Theorem Proving	Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
Schaefer fragments	Reintroducing the Second Player in EPR
SCL	Extending SMT Solving with Non-Ground Clause Learning
SCL(FOL)	Efficient Linear Model Building and Clause Evaluation
search heuristics	Some Experiments with Twee-Style Goal-Directedness
secure computing	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
security	NetKAT: Learning Models and Solving Equations
shared terms	Some Experiments with Twee-Style Goal-Directedness
Signal Temporal Logic	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
simplex	Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA
Simplification	Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
Simply-typed lambda calculus	de Vrijer's Strong Normalization in Haskell
SMT	Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification Reasoning About Hyperproperties with Automated Theorem Provers Extending SMT Solving with Non-Ground Clause Learning Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA Reasoning about Collections in SMT
SMT solvers	LLM-Assisted Formal Verification of Bit-vector Invertibility Conditions in Rocq
software verification	Reasoning About Hyperproperties with Automated Theorem Provers Bug-free embedded software: a realisable dream? (and how VerCors will help…)
SPASS(SCL)	Efficient Linear Model Building and Clause Evaluation
SQL	Using Formal Verification for the Text-to-SQL Task
stream reasoning	Stream Reasoning with Sequencing
Strong normalization	de Vrijer's Strong Normalization in Haskell
Superposition	Enhancing Superposition Reasoning in Linear Real Arithmetic through Selection and Simplification
symbolic	Induction and K-Induction for Hyperproperties
symmetry breaking	Coloring Queens with Thousands of Encodings
synthesis of reactive systems	Blinking Synthesis
T
Tableau Methods	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
Tableaux	First-Order Tableaux with Unification for Henkin Quantifiers Towards an Operational Proof-theoretic Semantics
termination	Cycle Detection for Affine Integer Linear Loops
Theorem Proving	Formally Solving Answer-Construction Problems in Lean
TPTP	Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB Benchmarking LLMs Against TPTP: A Vision for the Near Future
Tree-Shaped Tableau	STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas
type theory	Formalized Hopfield Networks and Boltzmann Machines A Formalized Neurodynamic Solver for $N$-Queens Completion
U
unification	Algebraic Indexing to Parallelize Atom Comparison in the ATP Saturation Loop
uniform proofs	Towards an Operational Proof-theoretic Semantics
V
Vampire	Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection Neural Conjecturing for Saturation Theorem Provers (short)
VerCors	Bug-free embedded software: a realisable dream? (and how VerCors will help…)
verification	Cycle Detection for Affine Integer Linear Loops
vipe-coding	Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA
W
Weakest preconditions	Towards a Proof-Theoretic Analysis of Incorrect/Incomplete Proofs
Wilkie's identity	A SAT Attack on Tarski's High School Algebra Problem
Z
Zero Knowledge Proofs	Scaling Zero Knowledge UNSAT Verification via Normalized Chaining

Disclaimer | Powered by EasyChair Smart Program