相关论文: Pure Prolog Execution in 21 Rules

Control code is a concept that is closely related to a frequently occurring practitioner's view on what is a program: code that is capable of controlling the behaviour of some machine. We present a logical approach to explain issues…

We explore a definition of complexity based on logic functions, which are widely used as compact descriptions of rules in diverse fields of contemporary science. Detailed numerical analysis shows that (i) logic complexity is effective in…

Inductions and game semantics are two useful extensions to traditional logic programming. To be specific, inductions can capture a wider class of provable formulas in logic programming. Adopting game semantics can make logic programming…

This is a survey on propositional proof complexity aimed at introducing the basics of the field with a particular focus on a method known as feasible interpolation. This method is used to construct "hard theorems" for several proof systems…

Game Logic is an excellent setting to study proofs-about-programs via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent's…

Both Prolog and Oz are multiparadigm languages with a logic programming core. There is a significant subset of Oz that is a syntactic variant of Prolog: pure Prolog programs with green or blue cuts and bagof/3 or setof/3 can be translated…

We describe the BinProlog system's compilation technology, runtime system and its extensions supporting first-class Logic Engines while providing a short history of its development, details of some of its newer re-implementations as well as…

Multiplicative linear logic is a very well studied formal system, and most such studies are concerned with the one-sided sequent calculus. In this paper we look in detail at existing translations between a deep inference system and the…

We propose a framework grounded in Logic Programming for representing and reasoning about business processes from both the procedural and ontological point of views. In particular, our goal is threefold: (1) define a logical language and a…

In this paper we propose an extension of Defeasible Logic to represent and compute three concepts of defeasible permission. In particular, we discuss different types of explicit permissive norms that work as exceptions to opposite…

This paper shows the debugging facilities provided by the SLAM system. The SLAM system includes i) a specification language that integrates algebraic specifications and model-based specifications using the object oriented model. Class…

One way to interpret the reasoning power of transformer-based language models is to describe the types of logical rules they can resolve over some input text. Recently, Chiang et al. (2023) showed that finite-precision transformers can be…

Logic programming, as exemplified by datalog, defines the meaning of a program as its unique smallest model: the deductive closure of its inference rules. However, many problems call for an enumeration of models that vary along some set of…

Large language model agents that use external tools are often implemented through reactive execution, in which reasoning is repeatedly recomputed after each observation, increasing latency and sensitivity to error propagation. This work…

Machine-specific optimizations command the machine to behave in a specific way. As current programming models largely leave machine details unexposed, they cannot accommodate direct encoding of such commands. In previous work we have…

In this paper, we characterize the properties of a direct interpretation of HPSG and present the advantages of this approach. High-level programming languages constitute in this perspective an efficient solution: we show how a…

Several Prolog implementations include a facility for tabling, an alternative resolution strategy which uses memoisation to avoid redundant duplication of computations. Until relatively recently, tabling has required either low-level…

Refinement transforms an abstract system model into a concrete, executable program, such that properties established for the abstract model carry over to the concrete implementation. Refinement has been used successfully in the development…

We propose utilizing background operators for mathematical reasoning in large language models (LLMs). To achieve this, we define a set of fundamental mathematical predicates as the basic building blocks. For each mathematical problem, we…

Lambda Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic…