ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 12 Issue 2, January 2011

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...