cs.LO · 2026-07-26 · No. 65
Logic in Computer Science, 2026-07-26.
12 new papers in cs.LO. Titles, authors,
abstracts. Links to arXiv. Want this in your inbox every morning? Subscribe →
01 — The papers
12 entries-
01
Scaling Up Formal Representation of Clinical Trial Protocols in Ensemble Logic Using LLMs: A Preliminary Study
Yan Huang, Xubing Hao, Xiaojin Li, Rashmie Abeysinghe, Xiaoqian Jiang, Licong Cui, Guo-Qiang Zhang
cs.LO · cs.AI · cs.ET
The reliance on unstructured free text for documenting clinical trial protocols creates a significant barrier to automated reasoning, cohort discovery, and trial simulation. The lack of formal structure obscures critical temporal phenotypes, such as dynamic eligibility criteria and event timing constraints. Although Temporal Ensemble Logic (TEL) offers an expressive framework for modeling these elements, manual encoding remains a prohibitive...
-
02
Explainable Belief Harmonization under Dynamic Epistemic Partitions
Adam Kostka, Jarosław A. Chudziak
cs.LO · cs.AI · cs.MA
Existing approaches to multi-agent belief combination have established mature foundations for combining uncertain beliefs under common assumptions: consensus methods use iterative averaging, logic-based methods resolve conflicting knowledge bases, and epistemic logic analyzes agents' information states. Typically, these approaches assume that the structure determining what each agent can represent remains fixed. However, in many scenarios,...
-
03
Explainability Framework for Policy-Aware Autonomous Agents
Heather Merhout, Daniela Inclezan
cs.LO · cs.AI
In the field of Artificial Intelligence, an agent is a system which is able to autonomously make decisions in order to reach a desired goal. As these systems grow more prevalent in our day-to-day lives, there has been an increased need to add explainability features which can provide an account for an agent's behavior. We therefore propose a framework that outlines how to produce comprehensible explanations for policy-aware agents, or agents...
-
04
Hybrid MKNF with Classical Negation in the Rule Component
Arun Raveendran Nair Sheela, Christophe Rey, Florence De Grancey
cs.LO · cs.AI · cs.SC
Hybrid MKNF knowledge bases under the well-founded semantics integrate Description Logics with Logic Programming. However, they do not support classical negation in the rule component, limiting their ability to represent explicit negative knowledge. This limitation is particularly significant in safety-critical applications, where reasoning often requires explicit negative information rather than interpreting the absence of information as...
-
05
Towards a Certifying Grounder
Daimy Van Caudenberg, Alexander Ek, Carlos Cantero, Bart Bogaerts
cs.LO · cs.AI
Grounding, the translation of high-level theories into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is not certifying, there is no way of knowing that the obtained solutions actually correspond to the original problem specification, resulting in a trust gap. In this paper, we close the trust gap between the user's high-level...
-
06
Declarative Problem Solving in UAM Strategic Deconfliction
Gioacchino Sterlicchio, Angelo Oddi, Riccardo Rasconi, Francesca Alessandra Lisi
cs.LO · cs.AI
The growing demand for Urban Air Mobility (UAM) introduces significant challenges in airspace management, particularly within densely populated metropolitan regions. As the number of aerial vehicles-such as drones, air taxis, and helicopters-continues to rise, so does the risk of mid-air collisions and conflicts with existing air traffic and obstacles. Ensuring safe and efficient UAM operations requires robust strategic deconfliction...
-
07
Case study: solving P-99 with LPTP and an LLM
Fred Mesnard, Thierry Marianne, Étienne Payet, Wim Vanhoof
cs.LO · cs.AI
Ninety-Nine Prolog Problems (P-99) is a famous set of Prolog exercises. We solved the first thirty three just by prompting an LLM (Large Language Model). We used Claude from Anthropic. By solved we mean: generate the Prolog code and a test file, run the tests and check whether they pass, then formally prove types, groundness, termination, uniqueness, existence and also sometimes functional correctness with LPTP (Logic Program Theorem Prover)....
-
08
Chess\_db: A framework for working with large chess game datasets
Nicos Angelopoulos, Jan Wielemaker
cs.LO · cs.AI · cs.DB · cs.SC
Chess is a two player strategic game that is embedded in classical AI culture as it was once the frontier for intelligent behaviour. There was the silent assumption that the advent of computer engines that play better than the best humans will extinguish interest in the game. However, the opposite has come to pass, with a growing following for the game. A lot of the computational resources are now centered around training of players, where...
-
09
Animation, Verification and Visualisation of Prolog Transition Systems with ProB
Jan Gruteser, Michael Leuschel, Katharina Engels, Fabian Vu
cs.LO · cs.AI · cs.GT
ProB is a Prolog-based model checker, animator and constraint solver for high-level formal specifications. One can also use ProB to animate transition systems defined by Prolog predicates, allowing the application of its various validation techniques. In this work, we present the existing features of ProB's Prolog animation mode and its recent extensions. The extended capabilities include simulation for statistical checks, more reliable trace...
-
10
Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB
Katharina Engels, Jan Gruteser, Michael Leuschel
cs.LO · cs.AI · cs.SE
Event-B is a formal method rooted in predicate logic and set theory. We encoded over 600 proof rules in Prolog, enabling a systematic, comprehensible proof analysis and construction. By integrating the proof rules into the Prolog-based validation tool ProB, we obtain an interactive proof system with proof tree visualisation. This has advantages in teaching, giving students direct control over the selection of proof rules. Our tool can import...
-
11
Case study: proving sqrt(2) irrational with LPTP and an LLM
Fred Mesnard, Étienne Payet, Wim Vanhoof
cs.LO · cs.AI · cs.SC
We present the interactions with an LLM (Large Language Model) aiming at proving that the square root of 2 is not a rational number in an LP (Logic Programming) context. We start from a few basic pure logic programming predicate definitions. We rely on the LPTP (Logic Program Theorem Prover) system for stating and proving properties about logic programs. As the proof language of LPTP is based on natural deduction, the proofs are human...
-
12
Anti-Goal Reasoning: Rethinking the Theory of Goal Reasoning in Non-Axiomatic Logic
Bowen Xu
cs.LO · cs.AI
Goal reasoning in Non-Axiomatic Logic (NAL) explains how an adaptive system derives means for realizing desired events under insufficient knowledge and resources. However, the representation of avoidance is less clear. A common convention is to express ``avoid $G$'' as the goal sentence ``$\neg G!$'', but this notation conflates two different readings: pursuing the negated event $\neg G$, and avoiding the positive event $G$. This paper shows...
This edition is part of The Daily Abstract — cs.LO archive. Subscribe to receive these in your inbox each morning, automatically translated to Spanish, with reply-to-PDF: arxivdaily.ignorelist.com.
#D99C5E. Built and served on an always-free VM. The masthead is set 14% letterspaced because newspapers do that and it works.