enter search term and/or author name
A uniform approach to constraint-solving for lists, multisets, compact lists, and sets
Agostino Dovier, Carla Piazza, Gianfranco Rossi
Article No.: 15
Lists, multisets, and sets are well-known data structures whose usefulness is widely recognized in various areas of computer science. They have been analyzed from an axiomatic point of view with a parametric approach in Dovier et al....
Foundational certified code in the Twelf metalogical framework
Karl Crary, Susmit Sarkar
Article No.: 16
Foundational certified code systems seek to prove untrusted programs to be safe relative to safety policies given in terms of actual machine architectures, thereby improving the systems' flexibility and extensibility. Using the Twelf metalogical...
Inferring non-suspension conditions for logic programs with dynamic scheduling
Samir Genaim, Andy King
Article No.: 17
A logic program consists of a logic component and a control component. The former is a specification in predicate logic whereas the latter defines the order of subgoal selection. The order of subgoal selection is often controlled with delay...
The following known observation is useful in establishing program termination: if a transitive relation R is covered by finitely many well-founded relations U1,…,Un then R is well-founded. A...
Abstract state machines capture parallel algorithms: Correction and extension
Andreas Blass, Yuri Gurevich
Article No.: 19
We consider parallel algorithms working in sequential global time, for example, circuits or parallel random access machines (PRAMs). Parallel abstract state machines (parallel ASMs) are such parallel algorithms, and the parallel ASM thesis asserts...
Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. Coverage metrics attempt to check...
We introduce a proof system for Hájek's logic BL based on a relational hypersequents framework. We prove that the rules of our logical calculus, called RHBL, are sound and invertible with respect to any valuation of BL...
Conjunctive query containment and answering under description logic constraints
Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini
Article No.: 22
Query containment and query answering are two important computational tasks in databases. While query answering amounts to computing the result of a query over a database, query containment is the problem of checking whether, for every database,...
The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this article we investigate the consequences of relativizing these concepts to explicitly specified contexts. We obtain contextual modal logic...