Sequent-type proof systems constitute an important and widely-used class of calculi well-suited for analysing proof search. In this paper, we introduce a sequent-type calculus for a variant of default logic employing ...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
Sequent-type proof systems constitute an important and widely-used class of calculi well-suited for analysing proof search. In this paper, we introduce a sequent-type calculus for a variant of default logic employing Lukasiewicz's three-valued logic as the underlying base logic. this version of default logic has been introduced by Radzikowska addressing some representational shortcomings of standard default logic. More specifically, our calculus axiomatises brave reasoning for this version of default logic, following the sequent method first introduced in the context of nonmonotonic reasoning by Bonatti, which employs a complementary calculus for axiomatising invalid formulas, taking care of expressing the consistency condition of defaults.
Answer Set programming (ASP) is a well-established declarative programming language based on logic. the success of ASP is mainly due to the availability of efficient ASP solvers, therefore their development is still a...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
Answer Set programming (ASP) is a well-established declarative programming language based on logic. the success of ASP is mainly due to the availability of efficient ASP solvers, therefore their development is still an important research topic. In this paper we report the recent improvements of the well-known ASP solver WASP. the new version of WASP includes several improvements of the main solving strategies and advanced reasoning techniques for computing paracoherent answer sets. Indeed, WASP is the first ASP solver handling paracoherent reasoning under two mainstream semantics, namely semi-stable and semiequilibrium. However, semi-equilibrium semantics may require the introduction of several disjunctive rules, which are usually considered as a source of inefficiency for modern solvers. Such a drawback is addressed in WASP by implementing ad-hoc techniques to efficiently handle disjunctive logic programs. these techniques are presented and evaluated in this paper.
Although parity constraints are at the heart of many relevant reasoning modes like sampling or model counting, little attention has so far been paid to their integration into ASP systems. We address this shortcoming a...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
Although parity constraints are at the heart of many relevant reasoning modes like sampling or model counting, little attention has so far been paid to their integration into ASP systems. We address this shortcoming and investigate a variety of alternative approaches to implementing parity constraints, ranging from rather basic ASP encodings to more sophisticated theory propagators (featuring Gauss-Jordan elimination). All of them are implemented in the xorro system by building on the theory reasoning capabilities of the ASP system dingo. Our comparative empirical study investigates the impact of the number and size of parity constraints on performance and indicates the merits of the respective implementation techniques. Finally, we benefit from parity constraints to equip xorro with means to sample answer sets, paving the way for new applications of ASP.
Claessen and Rosen have recently presented an automatedtheorem prover, intuit, for intuitionistic propositional logic which utilises a SAT-solver. We present a sequent calculus perspective of the theory underpinning ...
详细信息
ISBN:
(纸本)9783030290269;9783030290252
Claessen and Rosen have recently presented an automatedtheorem prover, intuit, for intuitionistic propositional logic which utilises a SAT-solver. We present a sequent calculus perspective of the theory underpinning intuit by showing that it implements a generalisation of the implication-left rule from the sequent calculus LJT, also known as G4ip and popularised by Roy Dyckhoff.
the ability to perform complex reasoning over data streams has recently become an important area of research in the Semantic Web community. Most of SPARQL-inspired engines have limitations in capturing sophisticated u...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
the ability to perform complex reasoning over data streams has recently become an important area of research in the Semantic Web community. Most of SPARQL-inspired engines have limitations in capturing sophisticated user requirements and dealing with complex reasoning tasks. To address these challenges, we propose and implement C-ASP, a reasoning system based on the Answer Set programming (ASP) system Clingo and extended to handle continuous reasoning requests over RDF streams. We provide the syntax of the C-ASP language, as well as a set of examples in order to illustrate its expressive power. In addition, we present preliminary experimental results showing C-ASP performances.
this paper presents so-called asl-explanation graphs for answer set programming based on a translation of extended logic programs to abstract dialectical frameworks (ADF). the graphs show how a literal can be derived ...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
this paper presents so-called asl-explanation graphs for answer set programming based on a translation of extended logic programs to abstract dialectical frameworks (ADF). the graphs show how a literal can be derived from the program, and they evaluate in an argumentative way why necessary assumptions about literals not contained in an answer set hold. Withthe set of all asl-explanation graphs for a literal and an answer set, it is possible to explain and justify thoroughly why the literal is or is not contained in that answer set. Additionally, we provide a criterion to improve the clarity of explanations by pruning nodes without loss of information and selecting most significant asl-explanation graphs.
In this paper we introduce a framework built on top of the Knowledge Base System IDP, which allows local search heuristics to be synthesized from their formal descriptions. It is introduced as a new inference to solve...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
In this paper we introduce a framework built on top of the Knowledge Base System IDP, which allows local search heuristics to be synthesized from their formal descriptions. It is introduced as a new inference to solve optimization problems in IDP. To model a local search heuristic, users need to specify its components, among which neighbourhood moves are the most important. Two types of neighbourhood moves, namely standard moves and Large Neighbourhood Search moves, are supported. A set of built-in local search heuristics are provided, allowing users to combine neighbourhoods in different ways. We demonstrate how the new local search inference can be used to complement the existing solving mechanisms for logicprogramming.
We present a logical framework allowing us to express assessment of facts (is it proven?) and arguments (is it sound?) together with a proof system to answer these questions. Our motivation is to clarify the notion of...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
We present a logical framework allowing us to express assessment of facts (is it proven?) and arguments (is it sound?) together with a proof system to answer these questions. Our motivation is to clarify the notion of validity in the context of logic-based arguments along different aspects (such as the formulas used and the inference scheme). Originality lies in the possibility for the user to design their own argument schemes. We show that classical inference obtains when arguments are based on classical schemes (e.g. Hilbert axioms). We go beyond classical logic by distinguishing "proven" formulas from "uncontroversial" ones (whose negation is not proven). Hence a formal definition of a fallacious argument: it uses controversial formulas or schemes recognized as illicit. We express some rational arguments and fallacies in the form of schemes.
Our ultimate goal is to conceive an extension of Answer Set programming with language constructs from dynamic (and temporal) logic to provide an expressive computational framework for modeling dynamic applications. To...
详细信息
ISBN:
(纸本)9783030205287;9783030205270
Our ultimate goal is to conceive an extension of Answer Set programming with language constructs from dynamic (and temporal) logic to provide an expressive computational framework for modeling dynamic applications. To address this in a semantically well founded way, we generalize the definition of Dynamic Equilibrium logic to accommodate finite linear time and extend it with a converse operator in order to capture past temporal operators. this results in a general logical framework integrating existing dynamic and temporal logics of Here-and-there over both finite and infinite time. In the context of finite time, we then develop a translation of dynamic formulas into propositional ones that can in turn be translated into logic programs.
logics based on the mu-calculus are used to model inductive and coinductive reasoning and to verify reactive systems. A well-structured proof-theory is needed in order to apply such logics to the study of programming ...
详细信息
ISBN:
(纸本)9783030290269;9783030290252
logics based on the mu-calculus are used to model inductive and coinductive reasoning and to verify reactive systems. A well-structured proof-theory is needed in order to apply such logics to the study of programming languages with (co)inductive data types and automated (co)inductive theorem proving. the traditional proof system suffers some defects, non-wellfounded (or infinitary) and circular proofs have been recognized as a valuable alternative, and significant progress have been made in this direction in recent years. Such proofs are nonwellfounded sequent derivations together with a global validity condition expressed in terms of progressing threads. the present paper investigates a discrepancy found in such proof systems, between the sequential nature of sequent proofs and the parallel structure of threads: various proof attempts may have the exact threading structure while differing in the order of inference rules applications. the paper introduces infinets, that are proof-nets for non-wellfounded proofs in the setting of multiplicative linear logic with least and greatest fixed-points (mu MLL infinity) and study their correctness and sequentialization.
暂无评论