Displaying similar documents to “Towards automated proofs of observational properties.”

Quasi-lines and their degenerations

Laurent Bonavero, Andreas Höring (2007)

Annali della Scuola Normale Superiore di Pisa - Classe di Scienze


In this paper we study the structure of manifolds that contain a quasi-line and give some evidence towards the fact that the irreducible components of degenerations of the quasi-line should determine the Mori cone. We show that the minimality with respect to a quasi-line yields strong restrictions on fibre space structures of the manifold.

Study of irreducible balanced pairs for substitutive languages

Julien Bernat (2008)

RAIRO - Theoretical Informatics and Applications


Let be a language. A balanced pair consists of two words and in which have the same number of occurrences of each letter. It is irreducible if the pairs of strict prefixes of and of the same length do not form balanced pairs. In this article, we are interested in computing the set of irreducible balanced pairs on several cases of languages. We make connections with the balanced pairs algorithm and discrete geometrical constructions related to substitutive languages. We characterize...

Homomorphic images of finite subdirectly irreducible unary algebras

Jaroslav Ježek, P. Marković, David Stanovský (2007)

Czechoslovak Mathematical Journal


We prove that a finite unary algebra with at least two operation symbols is a homomorphic image of a (finite) subdirectly irreducible algebra if and only if the intersection of all its subalgebras which have at least two elements is nonempty.

Experimental analysis of some computation rules in a simple parallel reasoning system for the ALC description logic

Adam Meissner (2011)

International Journal of Applied Mathematics and Computer Science


A computation rule determines the order of selecting premises during an inference process. In this paper we empirically analyse three particular computation rules in a tableau-based, parallel reasoning system for the ALC description logic, which is built in the relational programming model in the Oz language. The system is constructed in the lean deduction style, namely, it has the form of a small program containing only basic mechanisms, which assure soundness and completeness of reasoning....

Some Ramsey type theorems for normed and quasinormed spaces

C. Henson, Nigel Kalton, N. Peck, Ignác Tereščák, Pavol Zlatoš (1997)

Studia Mathematica


We prove that every bounded, uniformly separated sequence in a normed space contains a “uniformly independent” subsequence (see definition); the constants involved do not depend on the sequence or the space. The finite version of this result is true for all quasinormed spaces. We give a counterexample to the infinite version in L p [ 0 , 1 ] for each 0 < p < 1. Some consequences for nonstandard topological vector spaces are derived.