Related papers: Pure Prolog Execution in 21 Rules

This paper presents a simple notion of proof net for multiplicative linear logic with units. Cut elimination is direct and strongly normalising, in contrast to previous approaches which resorted to moving jumps (attachments) of par units…

Transition systems are often used to describe the behaviour of software systems. If viewed as a graph then, at their most basic level, vertices correspond to the states of a program and each edge represents a transition between states via…

Abstraction and realization are bilateral processes that are key in deriving intelligence and creativity. In many domains, the two processes are approached through rules: high-level principles that reveal invariances within similar yet…

Linear logic programming uses provability as the basis for computation. In the operational semantics based on provability, executing the additive-conjunctive goal $G_1 \& G_2$ from a program $P$ simply terminates with a success if both…

We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns…

We present strategic portgraph rewriting as a basis for the implementation of visual modelling and analysis tools. The goal is to facilitate the specification, analysis and simulation of complex systems, using port graphs. A system is…

To appear in Theory and Practice of Logic Programming (TPLP). Several Prolog interpreters are based on the Warren Abstract Machine (WAM), an elegant model to compile Prolog programs. In order to improve the performance several strategies…

Termination is an important and well-studied property for logic programs. However, almost all approaches for automated termination analysis focus on definite logic programs, whereas real-world Prolog programs typically use the cut operator.…

We interpret Linear Logic Proof Nets in a term language based on Solos calculus. The system includes a synchronisation mechanism, obtained by a conservative extension of the logic, that enables to define non-deterministic behaviours and…

This paper presents an environment for solving Prolog problems which has been implemented as a module for the virtual laboratory VILAB. During the problem solving processes the learners get fast adaptive feedback. As a result analysing the…

This paper describes a resolution based Description Logic reasoning system called DLog. DLog transforms Description Logic axioms into a Prolog program and uses the standard Prolog execution for efficiently answering instance retrieval…

We introduce proof nets for PiL, an extension of first-order multiplicative additive linear logic with new operators allowing a shallow encoding of processes in the {\pi}-calculus as formulas. We provide correctness criterion,…

We introduce ProofGrid, a benchmark suite for evaluating LLM reasoning through machine-checkable proofs rather than final answers alone. ProofGrid contains 15 tasks spanning proof writing, proof checking, proof masking, and proof…

Type inference is an application domain that is a natural fit for logic programming (LP). LP systems natively support unification, which serves as a basic building block of typical type inference algorithms. In particular, polymorphic type…

The problem we want to solve is how to generate all theorems of a given size in the implicational fragment of propositional intuitionistic linear logic. We start by filtering for linearity the proof terms associated by our Prolog-based…

We introduce SMProbLog, a generalization of the probabilistic logic programming language ProbLog. A ProbLog program defines a distribution over logic programs by specifying for each clause the probability that it belongs to a randomly…

Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic. We describe such a logic, the logic of compact closed categories and…

This book explores an alternative to the current dominant paradigm where a discrete computer model is constructed as an attempt to approximate some continuum theory. We focus on a class of discrete computer models that are based on simple…

Understanding how Large Language Models (LLMs) perform logical reasoning internally remains a fundamental challenge. While prior mechanistic studies focus on identifying taskspecific circuits, they leave open the question of what…

We present a straightforward embedding of quantified multimodal logic in simple type theory and prove its soundness and completeness. Modal operators are replaced by quantification over a type of possible worlds. We present simple…