Concept

Calcul des propositions

Publications associées (41)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

On Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

We explore the problem of automated reasoning about the non-disjoint combination of theories that share set variables and operations. We prove a combination theorem and apply it to show the decidability of the satisfiability problem for a class of formulas ...

2009

Combining Theories with Shared Set Operations

Viktor Kuncak, Ruzica Piskac

Motivated by applications in software verification, we explore automated reasoning about the non-disjoint combination of theories of infinitely many finite structures, where the theories share set variables and set operations. We prove a combination theore ...

Springer2009

Cryptographic protocol logic: Satisfaction for (timed) Dolev-Yao cryptography

Simon Kramer

This article is about a breadth-first exploration of logical concepts in cryptography and their linguistic abstraction and model-theoretic combination in a comprehensive logical system, called CPL (for Cryptographic Protocol Logic). We focus on two fundame ...

2008

Declarative Specification and Alignment Verification of Services in ITIL

Gil Regev, Alain Wegmann, Irina Rychkova

IT organizations that wish to implement the best practices recommended by the IT Infrastructure Library (ITIL) need to specify the level of service provided to their customers. The implemented service needs to comply with this specification. We propose a m ...

2008

Determining Significant Connectivity by 4D Spatiotemporal Wavelet Packet Resampling of Functional Neuroimaging Data

Dimitri Nestor Alice Van De Ville

An active area of neuroimaging research involves examining functional relationships between spatially remote brain regions. When determining whether two brain regions exhibit significant correlation due to true functional connectivity, one must account for ...

Elsevier2006

The Role of Tarski’s Declarative Semantics in the Design of Modeling Languages

Alain Wegmann, Andrey Naumenko

This paper focuses on Tarski

s declarative semantics and their usefulness in the design of a modeling language. We introduce the principles behind Tarski

s approach to semantics and explain what advantages this offers in the context of modeling languages. ...

2003

The Definition of Transitive Closure with OCL: Limitations and Applications

The Object Constraint Language (OCL) is based on first-order logic and set theory. As the most well-known application, OCL is used to formulate well-formedness rules in the UML metamodel. Here, the transitive closure of a relationship is defined in terms o ...

2003

Axiomatic theory of Sobolev spaces

Marc Troyanov

We develop an axiomatic approach to the theory of Sobolev spaces on metric measure spaces and we show that this axiomatic construction covers the main known examples (Hajlasz Sobolev spaces, weighted Sobolev spaces, Upper-radients, etc). We then introduce ...

2001

Observability and Controllability of Piecewise Affine and Hybrid Systems

Giancarlo Ferrari Trecate

In this paper we prove, in a constructive way, the equivalence between piecewise affine systems and a broad class of hybrid systems described by interacting linear dynamics, automata, and propositional logic. By focusing our investigation on the former cla ...

2000

Moving Horizon Estimation for Piecewise Affine Systems

Giancarlo Ferrari Trecate

Many practical control, estimation and fault detection problems involve hybrid systems, here losely defined as systems involving both continuous and discrete variables. Various approaches have been proposed for modeling hybrid systems. Often engineering sy ...

2000