This work presents the CMK knot coloring software system. CMK is a command-line tool written in SWI-Prolog that computes colorings of three-dimensional knots by finite quandles. The original purpose was to classify kn...
详细信息
ISBN:
(纸本)9781728176284
This work presents the CMK knot coloring software system. CMK is a command-line tool written in SWI-Prolog that computes colorings of three-dimensional knots by finite quandles. The original purpose was to classify knots by certain computational properties. CMK features a predicate that computes knot quandle presentations from braid words. The authors describe the key algorithms. Errors in five braid representations within the Mathematica(TM) KnotData collection are revealed through CMK.
The notion of forgetting, as considered in the famous paper by Lin and Reiter in 1994 has been extensively studied in classical logic and more recently, in non-monotonic formalisms like logic programming. In this pape...
详细信息
ISBN:
(纸本)9781577358350
The notion of forgetting, as considered in the famous paper by Lin and Reiter in 1994 has been extensively studied in classical logic and more recently, in non-monotonic formalisms like logic programming. In this paper, we convey the idea of forgetting to another major AI formalism, namely Dung-style argumentation frameworks. Our approach is axiomatic-driven and not limited to any specific semantics: we propose semantical and syntactical desiderata encoding different criteria for what forgetting an argument might mean;analyze how these criteria relate to each other;and check whether the criteria can be satisfied in general. The analysis is done for a number of widely used argumentation semantics. Our investigation shows that almost all desiderata are individually satisfiable. However, combinations of semantical and/or syntactical conditions reveal a much more interesting landscape. For instance, we found that the ad hoc approach to forgetting an argument, i.e., by the syntactical removal of the argument and all of its associated attacks, is too restrictive and only compatible with the two weakest semantical desiderata. Amongst the several interesting combinations identified, we showed that one satisfies a notion of minimal change and presented an algorithm that given an AF F and argument x, constructs a suitable AF G satisfying the conditions in the combination.
Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, ar...
详细信息
ISBN:
(数字)9783030449148
ISBN:
(纸本)9783030449148;9783030449131
Reduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem pro...
详细信息
ISBN:
(纸本)9783030510541;9783030510534
We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.
We study a dynamic version of multi-agent path finding problem (called D-MAPF) where existing agents may leave and new agents may join the team at different times. We introduce a new method to solve D-MAPF based on co...
详细信息
We study a dynamic version of multi-agent path finding problem (called D-MAPF) where existing agents may leave and new agents may join the team at different times. We introduce a new method to solve D-MAPF based on conflict-resolution. The idea is, when a set of new agents joins the team and there are conflicts, instead of replanning for the whole team, to replan only for a minimal subset of agents whose plans conflict with each other. We utilize answer set programming as part of our method for planning, replanning and identifying minimal set of conflicts.
We give an overview of the theory and practice of second-order rewriting. Second-order rewriting methods have been demonstrated as useful that is applicable to important notions of programming languages such as logic ...
详细信息
ISBN:
(纸本)9783030590246;9783030590253
We give an overview of the theory and practice of second-order rewriting. Second-order rewriting methods have been demonstrated as useful that is applicable to important notions of programming languages such as logic programming, algebraic effects, quantum computation, and cyclic computation. We explain foundation and evolution of second-order rewriting by presenting the framework of second-order computation systems. We also demonstrate our system SOL of second-order laboratory through various programming language examples.
We extend the lambda-calculus with constructs suitable for relational and functional-logic programming: non-deterministic choice, fresh variable introduction, and unification of expressions. In order to be able to uni...
详细信息
ISBN:
(纸本)9783030642761;9783030642754
We extend the lambda-calculus with constructs suitable for relational and functional-logic programming: non-deterministic choice, fresh variable introduction, and unification of expressions. In order to be able to unify lambda-expressions and still obtain a confluent theory, we depart from related approaches, such as lambda Prolog, in that we do not attempt to solve higher-order unification. Instead, abstractions are decorated with a location, which intuitively may be understood as its memory address, and we impose a simple coherence invariant: abstractions in the same location must be equal. This allows us to formulate a confluent small-step operational semantics which only performs first-order unification and does not require strong evaluation (below lambdas). We study a simply typed version of the system. Moreover, a denotational semantics for the calculus is proposed and reduction is shown to be sound with respect to the denotational semantics.
The design and implementation of a programming environment including an editor, a debugger and an interpreter engine for Lograph, a general-purpose visual logic programming language, is discussed. The rationale for us...
详细信息
The design and implementation of a programming environment including an editor, a debugger and an interpreter engine for Lograph, a general-purpose visual logic programming language, is discussed. The rationale for user-interface design decisions is presented, the goal of which is to increase cognitive support for the creation, exploration and debugging of Lograph programs. The design of the interpreter engine allows for animation of execution in the debugger. The engine takes full advantage of an efficient implementation of Prolog, and operates on a Prolog translation of Lograph programs and queries. The translated Lograph programs are probed with instrumentation code at appropriate places so that applications of Lograph rules are reported to the visual interface of the Lograph debugger as a side er effect of the execution of a program.
Concolic testing combines symbolic and concrete execution to generate test cases that achieve a good program coverage. Its benefits have been demonstrated for more than 15 years in the case of imperative programs. In ...
详细信息
ISBN:
(纸本)9783030590246;9783030590253
Concolic testing combines symbolic and concrete execution to generate test cases that achieve a good program coverage. Its benefits have been demonstrated for more than 15 years in the case of imperative programs. In this work, we present a concolic-based test generation tool for logic programs which exploits SMT-solving for constraint resolution.
In this paper, we revisit a temporal extension of Equilibrium logic (the logical characterisation of Answer Set programming) that introduces Linear Dynamic logic modalities. In particular, we further incorporate to th...
详细信息
ISBN:
(纸本)9781643681016;9781643681009
In this paper, we revisit a temporal extension of Equilibrium logic (the logical characterisation of Answer Set programming) that introduces Linear Dynamic logic modalities. In particular, we further incorporate to this extension (we call Linear Dynamic Equilibrium logic) an explicit negation operator, treated as a regular logical connective. We explain several formal properties of this new extension. For instance, we prove that some temporal operators that were not inter-definable, become so if we allow the use of explicit negation. Finally, we also introduce and study a new temporal operator called "while," that is an implicational dual of "until" and may be useful as a basic connective for temporal logic programming.
暂无评论