Theory & Algorithms · Computer Science & AI
Logic in Computer Science
The newest papers in Logic in Computer Science that ReadSearch has read, newest first. Each links to its own page, with its authors, date, where it was published and the original.
168 papers, from 4 September 2026 to 5 November 2026: 168 arXiv preprints.
Get the few papers worth your time in Logic in Computer Science every morning.
Follow Logic in Computer Science and ReadSearch reads its new papers each day, then brings you the few worth reading, each with its key finding in a sentence.
Newest papers, page 3
A Model-Theoretic Formalization of AlKhwaremis ilm alfaraid
This paper presents a model theoretic and computational formalization of AlKhwarizmis treatment of inheritance within the framework of Computational Fiqh.Numina Fuse: Interactive Autoformalization in Lean 4
Numina Fuse is an agent-native application for formalizing mathematics in Lean 4.Two Uncertainties Are Not One: Disagreement versus Decision-Risk in Cheap Structured Content Moderation
Content moderation compresses a graded, contested human judgment into a binary act (leave up / take down) over billions of items, at a scale where running a frontier LLM on every post is uneconomical.FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq
Quantum key distribution (QKD), whose security is derived from quantum mechanics rather than computational assumptions, is moving into standardization and commercial deployment.Global Convergence of Detailed Balanced Mass Action Systems
We give a self-contained proof that, for a finite detailed balanced mass-action system with positive rate constants, each positive stoichiometric compatibility class contains exactly one positive…Notation3: Graph Terms for RDF
Notation3 Logic was introduced as an extension of RDF allowing the user to express rules on top of triples and to make statements about graphs.PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions.VERDICT: Multi-Agent Parallel Modular Verification
Deductive verification scales to large software systems through modular reasoning, where formal contracts summarize the behavior of individual functions and enable their independent verification.TrustedCode: Evaluating Large Language Models for Developing Trusted Code through Automated Program Verification
Recent reports, such as "Who is using AI to code?", indicate that approximately 30\% of Python code contributions to GitHub are AI-generated.Local Allow, Global Deny: Why Per-Action Authorization Does Not Compose in LLM Agents
Autonomous LLM agents act through tools under per-action authorization: a local guard screens each tool call in isolation.Proof-Carrying Contracts: Commitments AI Agents Cannot Break
AI agents increasingly act on behalf of people or other agents, purchasing services, exchanging information and delegating work.Simply Logical -- The First Three Decades
This paper charts the evolution of the Prolog textbook Simply Logical -- Intelligent Reasoning by Example from print with runnable programmes on a 3.5-inch diskette published in 1994, via various…SLoSa: Small, Low-Power, and Safe Foundation Models for Robotic Task Planning
Safe robotic task planning requires planners that can reliably achieve task goals while satisfying safety constraints.Agentic Verified Optimization of Real-World Software
Program optimization aims to improve performance while preserving behavior.Beyond Leaderboards: A Method for Application-Specific Capability Profiling of Large Language Models
Public leaderboards rank large language models (LLMs) in general, but an engineer has to choose a model for a specific application, architecture and cost.On Counting Graphs for Modal Logic with Counting
In this paper, we study the theoretical computational complexity of counting trees and graphs that are classified positively by a graph neural networks, or said equivalently that satisfy a given…Theorem prover Arend
This paper is an exposition of the theorem prover Arend developed at JetBrains Research.Tactix: Towards a Programmable Strategy Interface for Flexible SAT Solving
Modern SAT solvers combine a rich repertoire of proof rules with sophisticated strategies that determine when and how to apply them.Verifying Human-Written Reasoning References
Evaluating the reasoning of AI systems often relies on human-written reasoning chains as references, yet the logical support for their individual steps is rarely verified.Controlled PROP: Theory and Applications to Quantum Circuits
Control is a fundamental concept in quantum and reversible computational models.