LPAR-26: Volume Information

Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning

Papers

Keyphrases

autoformalization, automata theory, automated reasoning³, automated theorem proving³, axiomatization, Benchmarks², Boltzmann machines, Boolos' curious inference, branching vector addition systems, Calculus of Inductive Constructions², cardinality constraints, CDCL, CEGAR, circuit equivalences, Claude Code, commonsense reasoning, comparison invariants, Comparison systems, complementation, computational complexity², control invariance, cut-introduction, Cyber-Physical Systems, de Vrijer's measure, decidable fragments, defeasible reasoning, dependent types, Description Logic, differential dynamic logic, eigenvariable conditions, English-to-logic translation, EPR, equational theories, equivalence relations, Event Calculus, finite model property, first-order logic, first-order theorem proving, formal mathematics, formal methods, Generalized Büchi Automata, Google Gemini, graph coloring, graph symmetry, greedy runs, Henkin quantifiers, high school identities, higher-order logic³, Higher order moments, Hopfield networks, Hybrid modal logic, hyperltl, Hyperproperties, imperfect information, induction, infinite-state systems, interactive theorem proving², invariant synthesis, ITP hammers, k-induction, knowledge representation², large language models³, Lean 4⁴, library alignment, linear arithmetic, literal selection, logic and types, many-sorted signatures, martingale, Maslov's class K, mathlib, modal logic², model checking², multiplicative substructural logic, natural language, neural clause-selection guidance, neural networks, optional stopping, pattern matching, PhysLib, probabilistic programs, program verification, proof checking, proof length, proof verification, proving strategies, PSPACE, Pushdown Games, QBF, queen's graph, Question Answering, Ramsey graphs, reachability, real arithmetic, redundancy, Requirements Engineering, Rocq², SAT, SAT encoding, satisfiability³, saturation-based theorem proving, Schaefer fragments, SCL, Signal Temporal Logic, simply typed lambda calculus, SMT⁵, software verification, Stream Reasoning, strong normalization, superposition, symmetry breaking, synthesis of reactive systems, tableau methods², theorem proving, TPTP, Tree-shaped Tableau, type theory, Vampire, Wilkie's identity, zero-knowledge proofs.