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.
logicprogramming has been used as a natural framework to automate deduction in the logic of order-of-magnitude reasoning. Specifically, we introduce a Prolog implementation of the Rasiowa-Sikorski proof system associ...
详细信息
logicprogramming has been used as a natural framework to automate deduction in the logic of order-of-magnitude reasoning. Specifically, we introduce a Prolog implementation of the Rasiowa-Sikorski proof system associated withthe relational translation Re(OM) of the multi-modal logic of order-of-magnitude qualitative reasoning OM.
An extension of DLV by aggregates to simplify the encoding of the frequently occuring concepts is discussed. DLV is an efficient Answer Set programming (ASP) system which can implement the answer set semantics with va...
详细信息
ISBN:
(纸本)354020721X
An extension of DLV by aggregates to simplify the encoding of the frequently occuring concepts is discussed. DLV is an efficient Answer Set programming (ASP) system which can implement the answer set semantics with various language extensions. the semantics of programs without aggregates is provided in BLR00 as an extension of the classical answer set semantics given in GL91. the strong point of DLV is its robust and efficient implementation, which integrates algorithms and heuristics from the field of nonmonotic reasoning.
We develop a sound, complete and practically implementable tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL(+) of the full Alternating time temporal logic ...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
We develop a sound, complete and practically implementable tableaux-based decision method for constructive satisfiability testing and model synthesis in the fragment ATL(+) of the full Alternating time temporal logic ATL*. the method extends in an essential way a previously developed tableaux-based decision method for ATL and works in 2EXP-TIME, which is the optimal worst case complexity of the satisfiability problem for ATL(+). We also discuss how suitable parameterizations and syntactic restrictions on the class of input ATL(+) formulae can reduce the complexity of the satisfiability problem.
We consider automatedreasoning about recursive partial functions with decidable domain, i.e. functions computed by incompletely defined but terminating functional programs. Incomplete definitions provide an elegant a...
详细信息
ISBN:
(纸本)354030553X
We consider automatedreasoning about recursive partial functions with decidable domain, i.e. functions computed by incompletely defined but terminating functional programs. Incomplete definitions provide an elegant and easy way to write and to reason about programs which may halt with a run time error by throwing an exception or printing an error message, e.g. when attempting to divide by zero. We investigate the semantics of incompletely defined programs, define an interpreter for those programs and discuss the termination of incompletely defined procedures. We then analyze which problems need to be solved if a theorem prover designed for verification of completely defined programs is modified to work for incompletely defined programs as well. We also discuss how to reason about stuck computations which arise when calling incompletely defined procedures with invalid arguments. Our method of automatedreasoning about incompletely defined programs has been implemented in the verification tool VeriFun. We conclude by discussing experiences obtained in several case studies withthis implementation and also compare and relate our proposal to other work.
TLA (the Temporal logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, withthe intent to ...
详细信息
ISBN:
(纸本)3540664920
TLA (the Temporal logic of Actions) is a linear temporal logic for specifying and reasoning about reactive systems. We define a subset of TLA whose formulas are amenable to validation by animation, withthe intent to facilitate the communication between domain and solution experts in the design of reactive systems.
We introduce StarExec, a public web-based service built to facilitate the experimental evaluation of logic solvers, broadly understood as automated tools based on formal reasoning. Examples of such tools include theor...
详细信息
ISBN:
(纸本)9783319085876;9783319085869
We introduce StarExec, a public web-based service built to facilitate the experimental evaluation of logic solvers, broadly understood as automated tools based on formal reasoning. Examples of such tools include theorem provers, SAT and SMT solvers, constraint solvers, model checkers, and software verifiers. the service, running on a compute cluster with 380 processors and 23 terabytes of disk space, is designed to provide a single piece of storage and computing infrastructure to logic solving communities and their members. It aims at reducing duplication of effort and resources as well as enabling individual researchers or groups with no access to comparable infrastructure. StarExec allows community organizers to store, manage and make available benchmark libraries;competition organizers to run logic solver competitions;and community members to do comparative evaluations of logic solvers on public or private benchmark problems.
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.
this position paper builds on the authors' previous work on paraconsistent transition systems to propose a modelling framework for quantum circuits with explicit representation of decoherence.
ISBN:
(纸本)9798400707551
this position paper builds on the authors' previous work on paraconsistent transition systems to propose a modelling framework for quantum circuits with explicit representation of decoherence.
暂无评论