the TPTP World is a well established infrastructure supporting research, development, and deployment of automatedtheorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logi...
详细信息
ISBN:
(纸本)9783642287176
the TPTP World is a well established infrastructure supporting research, development, and deployment of automatedtheorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logic, which in turn has enabled the integration of arithmetic. this paper describes these developments.
the proceedings contain 16 papers. the special focus in this conference is on logicprogramming. the topics include: Completeness of extended unification based on basic narrowing;implementation of full GHC by communic...
ISBN:
(纸本)9783540515647
the proceedings contain 16 papers. the special focus in this conference is on logicprogramming. the topics include: Completeness of extended unification based on basic narrowing;implementation of full GHC by communicating processes;inference methods and semantics on or-type knowledge bases;access program to minimize redundant refutations on the network database system;eUODHILOS: A general-purpose reasoning assistant system — Concept and implementation —;logic based lexical analyser LAX;extraction of characteristic facts and abstract generation;knowledge representation and reasoning for discourse understanding;proving definite clauses without explicit use of inductions;pseudo extension in default reasoning and belief revision by model inference;an approach to nonmonotonic inference mechanism in production system KORE/IE;nonmonotonic parallel inheritance network;logicprogramming debugger using control flow specification;aLEX: the logicprogramming language with explicit control and without cut-operators;lattice programming methodology;a simple programming system written in GHC and its reflective operations.
Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are ma...
详细信息
Building on the work of Burstall, this paper develops sound modelling and reasoning methods for imperative programs with pointers: heaps are modelled as mappings from addresses to values, and pointer structures are mapped to higher-level data types for verification. the programming language is embedded in higher-order logic. Its Hoare logic is derived. the whole development is purely definitional and thus sound. Apart from some smaller examples, the viability of this approach is demonstrated with a non-trivial case study. We show the correctness of the Schorr-Waite graph marking algorithm and present part of its readable proof in Isabelle/HOL. (c) 2005 Elsevier Inc. All rights reserved.
We show how to deploy the CIFF System 4.0 for abductive logicprogramming with constraints in a number of applications, ranging from combinatorial applications to web management. We also compare the CIFF System 4.0 wi...
详细信息
ISBN:
(纸本)9783540721994
We show how to deploy the CIFF System 4.0 for abductive logicprogramming with constraints in a number of applications, ranging from combinatorial applications to web management. We also compare the CIFF System 4.0 with a number of logicprogramming tools, namely the A-System, the DLV system and the SMODELS system.
We introduce a sequent calculus for bilattice-based annotated logic (BAL). We show that this logic can be syntactically and semantically translated into a fragment MSL* of conventional many-sorted logic MSL. We show d...
详细信息
ISBN:
(纸本)9783540730989
We introduce a sequent calculus for bilattice-based annotated logic (BAL). We show that this logic can be syntactically and semantically translated into a fragment MSL* of conventional many-sorted logic MSL. We show deductive equivalence of sequent calculus for BAL and sequent calculus for MSL*.
Computational Indistinguishability logic (CIL) is a logic for reasoning about cryptographic primitives in computational model. It is sound for standard model, but also supports reasoning in the random oracle and other...
详细信息
ISBN:
(数字)9783642412271
ISBN:
(纸本)9783642412271;9783642412264
Computational Indistinguishability logic (CIL) is a logic for reasoning about cryptographic primitives in computational model. It is sound for standard model, but also supports reasoning in the random oracle and other idealized models. We illustrate the benefits of CIL by formally proving the security of a Password-Based Key Exchange (PBKE) scheme, which is designed to provide entities communicating over a public network and sharing a short password, under a session key.
Norms and regulations play an important role in the governance of human society. Social rules Such as laws, conventions and contracts prescribe and regulate our behaviour, however it is possible for us to break these ...
详细信息
ISBN:
(纸本)9783642042379
Norms and regulations play an important role in the governance of human society. Social rules Such as laws, conventions and contracts prescribe and regulate our behaviour, however it is possible for us to break these rules at our discretion and face the consequences. By providing the means to describe and reason about norms in a computational context, normative frameworks may be applied to software systems allowing for automatedreasoning about the consequences of socially acceptable and unacceptable behaviour. In this paper, we outline our mathematical formulation for normative frameworks and describe how its semantics can be represented in ASP. thus enabling the construction of models of normative systems that can be subjected to formal verification and that can act as functional repositories of normative knowledge for the software components that participate in them.
the BQM1 system extends deductive database technology with knowledge structuring capabilities to provide an advanced environment for the development of data and knowledge-based applications. the system relies on a kno...
详细信息
ISBN:
(纸本)0818673125
the BQM1 system extends deductive database technology with knowledge structuring capabilities to provide an advanced environment for the development of data and knowledge-based applications. the system relies on a knowledge representation language that combines the declarativeness of logicprogramming withthe notions of object, inheritance with exceptions, and message passing. Exceptions are supported by allowing rules with negated heads. the use of exceptions inside the inheritance mechanism makes the language inherently nonmonotonic. the paper describes BQM focusing on boththe language and the implementation techniques. An informal overview of the language is first given. then, a number of techniques for efficient query evaluation are presented. these techniques significantly extend 'traditional' deductive database query evaluation strategies to deal with nonmonotonic reasoning. A description of the architecture of the current prototype of the BQM system is also given.
Well-known principles of induction include monotone induction and different sorts of non-monotone induction such as inflationary induction, induction over well-ordered sets and iterated induction. In this work, we def...
详细信息
ISBN:
(纸本)354020721X
Well-known principles of induction include monotone induction and different sorts of non-monotone induction such as inflationary induction, induction over well-ordered sets and iterated induction. In this work, we define a logic formalizing induction over well-ordered sets and monotone and iterated induction. Just as the principle of positive induction has been formalized in FO(LFP), and the principle of inflationary induction has been formalized in FO(IFP), this paper formalizes the principle of iterated induction in a new logic for Non-Monotone Inductive Definitions (NMID-logic). the semantics of the logic is strongly influenced by the well-founded semantics of logicprogramming. Our main result concerns the modularity properties of inductive definitions in NMID-logic. Specifically, we formulate conditions under which a simultaneous definition Delta of several relations is logically equivalent to a conjunction of smaller definitions Delta(1) boolean AND . . . boolean AND Delta(n) with disjoint sets of defined predicates. the difficulty of the result comes from the fact that predicates P-i and P-j defined in Delta(i) and Delta(j), respectively, may be mutually connected by simultaneous induction. Since logicprogramming and abductive logicprogramming under well-founded semantics are proper fragments of our logic, our modularity results are applicable there as well. As an example of application of our logic and theorems presented in this paper, we describe a temporal formalism, the inductive situation calculus, where causal dependencies axe naturally represented as rules of inductive definitions.
this paper gives a brief high-level description of the implementation of a disjunctive logicprogramming system referred to as DisLoP. this system is a result of research activities of the Disjunctive logic Programmin...
详细信息
ISBN:
(纸本)3540632557
this paper gives a brief high-level description of the implementation of a disjunctive logicprogramming system referred to as DisLoP. this system is a result of research activities of the Disjunctive logicprogramming-project (funded by Deutsche Forschungs-Gemeinschaft), undertaken by the University of Koblenz since July 1995.
暂无评论