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

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

A
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
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
Benchmarks	Challenging Benchmarks for Diagrammatic Equivalence of Circuits in TPTP and SMT-LIB Reasoning About Hyperproperties with Automated Theorem Provers
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	TBA
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	TBA
de Vrijer's measure	de Vrijer's Strong Normalization in Haskell
Decidable fragments of first-order logic	Pushing the Limits of Decidability: 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)
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	Pushing the Limits of Decidability: 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 model property	Pushing the Limits of Decidability: Maslov's class K with Equivalence
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
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
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	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
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
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
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 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	Pushing the Limits of Decidability: 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 Checking	Induction and K-Induction for Hyperproperties Reasoning About Hyperproperties with Automated Theorem Provers TBA
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	TBA
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
Optional stopping	Polynomial Invariants for Probabilistic Transition Systems with Unbounded Support
P
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	TBA
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
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	Pushing the Limits of Decidability: Maslov's class K with Equivalence
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
security	TBA
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 TBA
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…)
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
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
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