Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?

Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.

Découvrez-en plus sur les applications Graph.

Concept

Satisfiability modulo theories

En informatique et en logique mathématique, un problème de satisfiabilité modulo des théories (SMT) est un problème de décision pour des formules de logique du premier ordre avec égalité (sans quantificateurs), combinées à des théories dans lesquelles sont exprimées certains symboles de prédicat et/ou certaines fonctions. Des exemples de théories incluent la théorie des nombres réels, la théorie de l’arithmétique linéaire, des théories de diverses structures de données comme les listes, les tableaux ou les tableaux de bits, ainsi que des combinaisons de celles-ci. Instance d'un problème SMT Formellement, une instance de SMT est une formule du premier ordre sans quantificateur. Par exemple : (x1) \land (x = y+5) \land (y > 0) Le problème SMT est de déterminer si une telle formule est satisfiable par rapport à une théorie sous-jacente. Par exemple, on peut se demander si la formule ci-dessus est satisfiable par rapport à la théorie des nombres réels

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées

Chargement

Personnes associées

Chargement

Unités associées

Chargement

Concepts associés

Chargement

Cours associés

Chargement

Séances de cours associées

Chargement

Résumé

Source officielle

À propos de ce résultat

Publications associées (10)

Chargement

Afficher plus

Publications associées

Chargement

Personnes associées (2)

Personnes associées

Chargement

Unités associées (2)

Unités associées

Chargement

Concepts associés (18)

La démonstration automatique de théorèmes (DAT) est l'activité d'un logiciel qui démontre une proposition qu'on lui soumet, sans l'aide de l'utilisateur. Application en mathématiques Le

vignette|Une instance du Sudoku peut être transformée en une formule de logique propositionnelle à satisfaire. Une assignation des variables propositionnelles donne une grille complétée. En informatiq

Les problèmes de satisfaction de contraintes ou CSP (Constraint Satisfaction Problem) sont des problèmes mathématiques où l'on cherche des états ou des objets satisfaisant un certain nombre de contra

Afficher plus

Concepts associés

Chargement

Cours associés (1)

Cours associés

Chargement

Séances de cours associées (1)

Séances de cours associées

Chargement

A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Joseph Reynolds

We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson-Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from theories developed with Isabelle demonstrates the potential of the procedure.

Springer-Verlag Berlin2015

Chargement

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Andrew Joseph Reynolds

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux calculus for that fragment which uses as oracles a decision procedure for linear integer arithmetic and a number of computable functions over regular expressions. A distinguishing feature of this calculus is that it provides a completely algebraic method for solving membership constraints which can be easily integrated into multi-theory SMT solvers. Another is that it can be used to generate symbolic solutions for such constraints, that is, solved forms that provide simple and compact representations of entire sets of complete solutions. The calculus is part of a larger one providing the theoretical foundations of a high performance theory solver for string constraints implemented in the SMT solver CVC4.

Springer-Verlag Berlin2015

Chargement

ShapeOp - A Robust and Extensible Geometric Modelling Paradigm

Sofien Bouaziz, Anders Holden Deleuran, Bailin Deng, Mario Moacir Deuss, Mark Pauly

We present ShapeOp, a robust and extensible geometric modelling paradigm. ShapeOp builds on top of the state-of-the-art physics solver (Bouaziz et al. in ACM Trans Graph 33:154:1–154:11, 2014). We discuss the main theoretical advantages of the underlying solver and how this influences our modelling paradigm. We provide an efficient open-source C++ implementation (www.shapeop.org) together with scripting interfaces to enable ShapeOp in Rhino/Grasshopper and potentially other tools. This implementation can also act as a template for future integration of computer graphics research. To evaluate the potential of ShapeOp we present various examples using our implementation and discuss potential implications on the design process.

Springer 2015

Chargement

Afficher plus

La démonstration automatique de théorèmes (DAT) est l'activité d'un logiciel qui démontre une proposition qu'on lui soumet, sans l'aide de l'utilisateur. Application en mathématiques Le

Afficher plus

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.