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 6
Scenario-Based Compositional Statistical Model Checking for Safety Specifications
In safety-critical domains such as autonomous driving, systems must be evaluated across a large number of environment conditions, often represented as composite scenarios built from primitive…Formalizing the Moral Evaluation of Speech Acts: Truthfulness, Lies and Ethical Dilemmas
In life-or-death situations, a benevolent lie may appear more moral than telling the truth.RAOA: Alternating-Operator Neural Computation with Programmable Radio Propagation
Can programmable radio propagation serve as computational depth rather than only as a communication channel or one-shot analog transform?VeriPy Source-Preserving Verification and Compatibility Checking for Python Components
Keeping a Python program and its formal guarantees aligned is a continuing maintenance problem.Response Variability and Stability in Human Reasoning
Understanding how humans reason -- and how reasoning responses vary across tasks and individuals -- remains a core challenge for modeling and explanation in cognitive science.Solving VeriContest with a Lean-Backed Rust Verifier
VeriContest is a benchmark of 1007 competitive-programming problems in Rust, each with a Verus specification, a judge-accepted solution, and a Verus proof.FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification
Coding agents increasingly automate Lean proof development, but successful compilation alone does not establish that a candidate proves the intended statement under acceptable assumptions.An ontology for cross-sectoral crisis management: core and public health modules
This paper presents the European Crisis Management Ontology (ECMO), a modular OWL-based ontology intended as a cross-sectoral reference for disaster risk reduction and response.Hob-VL: A Benchmark for Visually Grounded Boolean Reasoning
Reliable visual reasoning requires composing multiple visual observations and returning consistent answers to logically equivalent questions.Q-Learning for Reachability in MEC-Free MDPs
Reinforcement learning (RL) for reachability specifications is fundamental to sequential decision-making.Premonoidal Semantics and Scalable Diagrammatics of Fermionic Quantum Computing
Local fermionic mode (LFM) based quantum computation has pure state spaces that are isomorphic, via the Jordan-Wigner representation, to qubit state spaces, but its compositional structure is subtly…Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over {H,X,C-NOT}: CSS Constructions, Soundness, and Mutation-Based Validation
Formal verification of quantum circuits becomes difficult as circuit size grows because exhaustive reasoning over the Hilbert space is computationally expensive.ProsaBuddy: Assisting Mechanized Real-Time Schedulability Analysis with LLM-based Agents
Rigorous schedulability analysis is essential for the design of hard real-time systems, yet errors in pen-and-paper proofs threaten the safety of critical applications.From Verification Failures to Reusable Guidance for Coding Agents
Coding agents need to establish that a program satisfies a specification and that the specification captures the requested behavior.Security Properties of Neural Networks as Decision Problems
Certifying a deployed neural network raises decision problems that the verification literature has not classified: whether the model carries a backdoor planted in its training data, whether a fault…A Simple Doxastic Deontic Logic for Norm-Guided Decision Making
Making decisions despite conflicting norms and incomplete or unreliable information is a fundamental challenge for autonomous systems.GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research
We present GenLimitLib, a source-aligned Lean 4 library for language generation in the limit.HyDI: A hybrid Deep Learning-Inductive Logic Programming ensemble for multi-label classification
While attaining remarkable results for many applications, Deep Learning models are notoriously difficult to explain.What Was Said, Not What Was 'Thought': Type-6 Logic for CoT Verification
We introduce Type-6 logic, a variant of dynamic epistemic logic augmented with two operators (uncertainty and recurrence), designed to model the inferential dynamics of contemporary large language…When Does Structured Knowledge Help Neural Theorem Proving?
Does structured mathematical knowledge help LLMs prove theorems in Lean 4?