60 papers
This paper demonstrates that while inquisitive team logic is expressively equivalent to first-order logic for sentences, its open formulas possess strictly greater expressive power, a finding that extends to standard inquisitive first-order logic where certain sentences can express non-first-order properties.
This paper presents the proceedings of the Eighth International Conference on Applied Category Theory (ACT2025), held at the University of Florida in June 2025, which featured a diverse collection of contributions spanning pure and applied disciplines such as computer science, quantum computation, and chemistry.
This paper introduces Elenchus, a dialogue system that leverages prover-skeptic interactions between a human expert and an LLM to construct knowledge bases grounded in inferentialist semantics, mapping dialectical states to formal logic to explicitly capture and verify the inferential relationships and design rationales of complex ontologies like PROV-O.
BemaGANv2 is an advanced GAN-based vocoder that enhances long-term audio generation for Text-to-Music and Text-to-Audio applications by integrating Anti-aliased Multi-Periodicity composition modules in the generator and systematically evaluating novel discriminator combination strategies, including the Multi-Envelope Discriminator, to achieve high-fidelity and temporally coherent results.
The paper introduces FATE, a new formal algebra benchmark series spanning from undergraduate exercises to PhD-level research problems, which reveals that current state-of-the-art LLMs struggle significantly with formalizing advanced mathematical reasoning, achieving near-zero accuracy on the most difficult tasks despite stronger natural-language performance.
This paper reports the discovery of a critical error in the 2006 Maniatis et al. analysis of the two Higgs doublet model potential's stability, which was identified through formalization in the Lean theorem prover and represents the first known non-trivial error in a physics paper uncovered by this rigorous method.
This paper establishes the decidability of the Skolem Problem for linear recurrence sequences in finitely generated commutative rings of positive characteristic by proving that their zero sets are effectively finite unions of -normal sets, leveraging recent advances in solving S-unit equations and linear equations over multiplicatively independent numbers.
This paper develops a higher-order abstract GSOS framework that represents operational semantics via pointed higher-order GSOS laws, thereby establishing general compositionality results for higher-order languages like the SKI and -calculi.
This paper presents a constructive formalization of Abstract Rewriting Systems in Agda that eliminates classical logic from standard proofs, refines termination and confluence criteria, and demonstrates its applicability through a formalization of the lambda calculus.
This paper proposes a consistency-based abductive reasoning framework that integrates predictions from multiple pre-trained models at test-time by formulating error management as a logic-constrained optimization problem, thereby significantly improving robustness and accuracy in novel environments with distributional shifts compared to individual models and standard ensembles.
This paper introduces Weighted Model Enumeration (WME) as a distinct solver-level task and presents complementary CDCL-based algorithms that integrate weight propagation, pruning, and conflict analysis into both chronological and non-chronological backtracking frameworks to efficiently enumerate weighted models.
This paper presents a Coq-based formalization that extends Tarski's mereogeometry into a full topological space by proving the correspondence between mereological classes and regular open sets, thereby reducing Tarski's axiomatic system and enhancing its expressiveness for Euclidean geometric reasoning.
This paper introduces a novel SAT-based approach for connection calculi in first-order logic that encodes the proof search structure itself, presenting three distinct encodings with symmetry breaking and implementing them in the new solver upCoP to advance automated reasoning.
This paper demonstrates that while bounded Turing machines cannot achieve self-certification due to temporal overhead, the iterative advancement of finite halting observations forms an ascending -chain whose Scott limit yields the least fixed point, effectively resolving the halting problem through the continuous deferral of diagonalization.
This paper establishes that the compactness of a finite relational structure is provable within Zermelo-Fraenkel set theory if the structure has width one, but implies the existence of non-measurable sets in three-dimensional space otherwise.
This paper presents formal proofs in Lean 4 of Farkas-like theorems over linearly ordered fields and extends duality theory to linear optimization problems where coefficients may take infinite values.
LTLGuard is a modular framework that enables resource-efficient open-weight language models (4B–14B parameters) to generate correct and conflict-free Linear Temporal Logic (LTL) specifications from informal requirements by combining constrained generation with lightweight symbolic reasoning for iterative consistency checking and refinement.
This paper introduces a formal framework for "model change" in description logic concepts, distinguishing between eviction, reception, and revision, and demonstrates that revision is a distinct operation that cannot be simply reduced to a combination of the other two while analyzing their compatibility within EL and ALC logics.
This paper proposes a neuro-symbolic approach that synergistically integrates Large Language Models with constraint solvers to iteratively generate and verify auxiliary lemmas, thereby significantly improving the ability to solve constraints involving inductive definitions compared to state-of-the-art solvers.
This paper introduces a categorical notion of "explanation" between probabilistic models using spans, demonstrating that every locally-finite probabilistic theory admits a canonical, sharp classical representation through a functorial construction.