Search ACM DL

Search Issue

enter search term and/or author name

**Logic of infons**: The propositional case

Yuri Gurevich, Itay Neeman

Article No.: 9

DOI: 10.1145/1877714.1877715

Infons are statements viewed as containers of information (rather then representations of truth values). The logic of infons turns out to be a conservative extension of logic known as constructive or intuitionistic. Distributed Knowledge...

**Safety alternating automata on data words**

Ranko Lazić

Article No.: 10

DOI: 10.1145/1877714.1877716

A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. Safety one-way alternating automata with one register on infinite data words are...

**Well-founded semantics for description logic programs in the semantic web**

Thomas Eiter, Giovambattista Ianni, Thomas Lukasiewicz, Roman Schindlauer

Article No.: 11

DOI: 10.1145/1877714.1877717

The realization of the Semantic Web vision, in which computational logic has a prominent role, has stimulated a lot of research on combining rules and ontologies, which are formulated in different formalisms. In particular, combining logic...

**Monadic second order logic on graphs with local cardinality constraints**

Stefan Szeider

Article No.: 12

DOI: 10.1145/1877714.1877718

We introduce the class of MSO-LCC problems, which are problems of the following form. Given a graph *G* and for each vertex *v* of *G* a set α(*v*) of non-negative integers. Is there a set *S* of vertices or edges of...

**The tractability of model checking for LTL**: The good, the bad, and the ugly fragments

Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer

Article No.: 13

DOI: 10.1145/1877714.1877719

In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If in contrast, the set of...

**Annotated probabilistic temporal logic**

Paulo Shakarian, Austin Parker, Gerardo Simari, Venkatramana V. S. Subrahmanian

Article No.: 14

DOI: 10.1145/1877714.1877720

The semantics of most logics of time and probability is given via a probability distribution over *threads*, where a thread is a structure specifying what will be true at different points in time (in the future). When assessing the...

**Mechanizing the metatheory of LF**

Christian Urban, James Cheney, Stefan Berghofer

Article No.: 15

DOI: 10.1145/1877714.1877721

LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's judgments....

**Persistent queries in the behavioral theory of algorithms**

Andreas Blass, Yuri Gurevich

Article No.: 16

DOI: 10.1145/1877714.1877722

We propose an extension of the behavioral theory of interactive sequential algorithms to deal with the following situation. A query is issued during a certain step, but the step ends before any reply is received. Later, a reply arrives, and later...

**MWeb**: A principled framework for modular web rule bases and its semantics

Anastasia Analyti, Grigoris Antoniou, Carlos Viegas Damasio

Article No.: 17

DOI: 10.1145/1877714.1877723

We present a principled framework for modular Web rule bases, called MWeb. According to this framework, each predicate defined in a rule base is characterized by its defining reasoning mode, scope, and exporting rule base list. Each predicate used...