The Dagstuhl Initiative for systematic benchmarking in answer set programming (ASP) is discussed. Benchmarking is needed in ASP to establish a good practices in the fields of satisfiablity testing and constraint progr...
详细信息
ISBN:
(纸本)354020721X
The Dagstuhl Initiative for systematic benchmarking in answer set programming (ASP) is discussed. Benchmarking is needed in ASP to establish a good practices in the fields of satisfiablity testing and constraint programming. The ASP is facing difficulty of not having a common input language and disagreement on all functionalities. The benchmarking system facilitates the execution of ASP solvers under the same conditions, quaranteeing reproducible and reliable performance outputs.
A system for parallel proofs is proposed. This system proves the inconsistency of formulas in the disjunctive-normal-forms. The system is a meta-system of Horn clauses (meta-rules) of a meta-predicate Prov which repre...
详细信息
ISBN:
(纸本)0780382781
A system for parallel proofs is proposed. This system proves the inconsistency of formulas in the disjunctive-normal-forms. The system is a meta-system of Horn clauses (meta-rules) of a meta-predicate Prov which represents a clause. A parallelism other than or- parallelism and the reduction of proving procedures with or-parallelism are shown. The efficiency is quantitatively shown for a simple case by estimating the complexity with or parallelism defined by the number of matching steps needed for the proof. A feature of the system is that any set of clauses can be represented as one meta-rule by using the disjunctive-normal-form. This fact shows new approaches to the parallelism and the use of lemmas. The soundness and the completeness of the system are proved.
We give a logic programming based account of probability and describe a declarative language P-log capable of reasoning which combines both logical and probabilistic arguments. Several non-trivial examples illustrate ...
详细信息
ISBN:
(纸本)354020721X
We give a logic programming based account of probability and describe a declarative language P-log capable of reasoning which combines both logical and probabilistic arguments. Several non-trivial examples illustrate the use of P-log for knowledge representation.
This paper investigates the optimization by fold/unfold of declarative programs that integrate the best features from both functional and logic programming. Transformation sequences are guided by a mixed strategy whic...
详细信息
ISBN:
(纸本)3540238069
This paper investigates the optimization by fold/unfold of declarative programs that integrate the best features from both functional and logic programming. Transformation sequences are guided by a mixed strategy which, in three low-level transformation phases. successfully combines two well-known heuristics -composition and tupling-, thus avoiding the construction of intermediate data structures and redundant. sub-computations. In particular, whereas composition is able to produce a single function definition for some nested (composed) functions. the tupling method merges non-nested functions calls into a new, function definition called eureka. We solve the non trivial problem of discovering the set of calls to be tupled in an incremental way.. i.e. chaining different eureka definitions where only non-nested calls sharing common variables are taken into account. Moreover, by appropriately combining both strategies, together with a simplification pre-process based on a kind of normalization, we automatically optimize a wide range of programs (with nested and/or non-nested function calls) at a very low cost.
We present SATMC (SAT-based Model Checker), an open and flexible platform for SAT-based bounded model checking [8] of security protocols. Under the standard assumptions of perfect cryptography and of strong typin...
详细信息
ISBN:
(数字)9783540302278
ISBN:
(纸本)3540232427
We present SATMC (SAT-based Model Checker), an open and flexible platform for SAT-based bounded model checking [8] of security protocols. Under the standard assumptions of perfect cryptography and of strong typing, SATMC performs a bounded analysis of the problem by considering scenarios with a finite number of sessions whereby messages are exchanged on a channel controlled by the most general intruder based on the Dolev-Yao model [12].
Total correctness assertions (TCAs) have long been considered a natural formalization of successful program termination. However, research dating back to the 1980s suggests that validity of TCAs is a notion of limited...
详细信息
ISBN:
(纸本)0769521924
Total correctness assertions (TCAs) have long been considered a natural formalization of successful program termination. However, research dating back to the 1980s suggests that validity of TCAs is a notion of limited interest;we corroborate this by proving compactness and Herbrand properties for the valid TCAs, defining in passing a new sound, complete, and syntax-directed deductive system for TCAs. It follows that proving TCAs whose truth depends on underlying inductive data-types is impossible in logics of programs that are sound for all structures, such as Dynamic logic based on Segerberg's PDL, even when augmented with powerful first-order theories like Peano Arithmetic. Harel's Convergence Rule bypasses this difficulty, but is methodologically and conceptually problematic, in addition to being unsound for general validity. We propose instead to bind variables to inductive data via DL's box operator, leading to an alternative formalization of termination assertions, which we dub Inductive TCA (ITCA). We observe that a TCA is provable in Harel's DL exactly when the corresponding ITCA is provable in Segerbegs's DL, thereby showing that the Convergence Rule is not foundationally or practically necessary. We also show that validity of ITCAs is directly reducible to validity of partial correctness assertions, confirming the foundational importance of the latter.
Prioritized logic Programs (PLPs) [7] introduce explicit representation of priorities to logic programs. They realize various types of (prioritized) commonsense reasoning in artificial intellig...
详细信息
ISBN:
(数字)9783540302278
ISBN:
(纸本)3540232427
Prioritized logic Programs (PLPs) [7] introduce explicit representation of priorities to logic programs. They realize various types of (prioritized) commonsense reasoning in artificial intelligence including preference abduction [5]. Recently, the authors realize a sound and complete procedure for computing preferred answer sets of a PLP [8]. The procedure uses techniques of answer set programming (ASP) [6], and also extends the original PLP by accommodating dynamic preferences in the language. The PLP procedure is implemented on top of the ASP solver DLV [3] using C++, and is now running under the Linux/Windows operating systems as “the PLP system”. The system is available at the URL: http://***/***, which provides binaries of the current release and the instruction on how to use the system. Some examples are also found there.
Understanding the logical meaning of any description logic or similar formalism is difficult for most people, and OWL-DL, is no exception. This paper presents the most common difficulties encountered by newcomers to t...
详细信息
ISBN:
(纸本)3540233407
Understanding the logical meaning of any description logic or similar formalism is difficult for most people, and OWL-DL, is no exception. This paper presents the most common difficulties encountered by newcomers to the language, that have been observed during the course of more than a dozen workshops, tutorials and modules about OWL-DL and it's predecessor languages. It emphasises understanding the exact meaning of OWL expressions - proving that understanding by paraphrasing them in pedantic but explicit language. It addresses, specifically, the confusion which OWL's open world assumption presents to users accustomed to closed world systems such as databases, logic programming and frame languages. Our experience has had a major influence in formulating the requirements for a new set of user interfaces for OWL the first of which are now available as prototypes. A summary of the guidelines and paraphrases and examples of the new interface are provided. The example ontologies are available online.
In this paper, a method to divide a large-scale logic program is proposed. The hierarchical structure of the given logic program can be found by using graph theory. An Illustrative example of elevator control program ...
详细信息
ISBN:
(纸本)9780780387300
In this paper, a method to divide a large-scale logic program is proposed. The hierarchical structure of the given logic program can be found by using graph theory. An Illustrative example of elevator control program is shown as application of the proposed theory.
In Semantic Web, using rules to add more expressive power has drawn considerable attention. Recently ORL (OWL Rules Language) has been presented where OWL is extended with Horn clause rules. In this paper we propose a...
详细信息
ISBN:
(纸本)3540238425
In Semantic Web, using rules to add more expressive power has drawn considerable attention. Recently ORL (OWL Rules Language) has been presented where OWL is extended with Horn clause rules. In this paper we propose an extension to OWL with more general rules involving not only atoms but also literals with classical negation and negation as failure. We present first the abstract syntax for our OWL extension and then its semantics via the Answer Set programming(ASP). Furthermore, we discuss the iterative procedures for reasoning between OWL axioms and ASP rules.
暂无评论