This paper describes an implementation of narrowing, an essential component of implementations of modern functional logic languages. These implementations rely on narrowing, in particular on some optimal narrowing str...
详细信息
ISBN:
(纸本)158113388X
This paper describes an implementation of narrowing, an essential component of implementations of modern functional logic languages. These implementations rely on narrowing, in particular on some optimal narrowing strategies, to execute functional logic programs. We translate functional logic programs into imperative (Java) programs without an intermediate abstract machine. A central idea of our approach is the explicit representation and processing of narrowing computations as data objects. This enables the implementation of operationally complete strategies (i.e., without back-tracking) or techniques for search control (e.g., encapsulated search). Thanks to the use of an intermediate and portable representation of programs, our implementation is general enough to be treed as a common back end for a wide variety of functional logic languages.
The PARMC system performs modelc hecking for systems described in the XL language, a variant of CCS. Extending previous work by Dong and Ramakrishnan that compiled XL specifications into an optimized transition relati...
详细信息
The goal of this project is to develop solutions to enhance interoperability between bioinformatics applications. Most existing applications adopt different data formats, forcing biologists into tedious translation wo...
详细信息
Simultaneous spatial constraint problems can be approached algebraically, geometrically, or constructively. We examine how each approach performs, using several example problems, especially constraint problems involvi...
详细信息
When Prolog programs that manipulate lists to manage a collection of resources are rewritten to take advantage of the linear logic resource management provided by the logicprogramming language Lolli, they can obtain ...
详细信息
The proceedings contain 59 papers. The special focus in this conference is on Description, Modal and Temporal logics. The topics include: Program termination analysis by size-change graphs;SET cardholder registration;...
ISBN:
(纸本)3540422544
The proceedings contain 59 papers. The special focus in this conference is on Description, Modal and Temporal logics. The topics include: Program termination analysis by size-change graphs;SET cardholder registration;algorithms, datastructures and other issues in efficient automated deduction;NExpTime-complete description logics with concrete domains;exploiting pseudo models for TBox and ABox reasoning in expressive description logics;the inverse method implements the automata approach for modal satisfiability;deduction-based decision procedure for a clausal miniscoped fragment of FTL;tableaux for temporal description logic with constant domains;free-variable tableaux for constant-domain quantified modal logics with rigid and non-rigid designation;instructing equational set-reasoning with otter;NP-completeness of refutability by literal-once resolution;ordered resolution vs. connection graph resolution;a model-based completeness proof of extended narrowing and resolution;a resolution-based decision procedure for the two-variable fragment with equality;superposition and chaining for totally ordered divisible abelian groups;on the evaluation of indexing techniques for theorem proving;preferred extensions of argumentation frameworks;bunched logicprogramming;a top-down procedure for disjunctive well-founded semantics;a second-order theorem prover applied to circumscription;a system for non-monotonic reasoning with logic programs under answer set semantics;conditional pure literal graphs;evaluating search heuristics and optimization techniques in propositional satisfiability;a system for deciding quantified boolean formulas satisfiability;a disconnection calculus theorem prover;more on implicit syntax;termination and reduction checking for higher-order logic programs;integrating connection-based theorem proving into interactive proof assistants and the extended least number heuristic.
The coincidence between the model-theoretic and the procedural semantics of SLD-resolution does not carry over to a Prolog system that also implements non-logical features like cut and whose depth-first search strateg...
详细信息
Cutting planes were introduced in 1958 by Gomory in order to solve integer linear optimization problems. Since then, they have received a lot of interest, not only in mathematical optimization, but also in logic and c...
详细信息
ISBN:
(纸本)3540672818
Cutting planes were introduced in 1958 by Gomory in order to solve integer linear optimization problems. Since then, they have received a lot of interest, not only in mathematical optimization, but also in logic and complexity theory. In this paper, we present some recent results on cutting planes at the interface of logic and optimization. Main emphasis is on the length and the rank of cutting plane proofs based on the Gomory-Chvatal rounding principle.
This paper presents an abstract treatment of the foundations of rewriting logic, generalising in three ways: an arbitrary 2-category plays the role of the specific 2-category Cat;the foundations are rendered fully ind...
详细信息
In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers ...
详细信息
ISBN:
(纸本)3540672818
In proof planning mathematical objects with theory-specific properties have to be constructed. More often than not, mere unification offers little support for this task. However, the integration of constraint solvers into proof planning can sometimes help solving this problem. We present such an integration and discover certain requirements to be met in order to integrate the constraint solver's efficient activities in a way that is correct and sufficient for proof planning. We explain how the requirements can be met by n extension of the constraint solving technology and describe their implementation in the constraint solver CoSIE.
暂无评论