Démonstration formelle

Résumé

Une démonstration formelle est une séquence finie de propositions (appelées formules bien formées dans le cas d'un langage formel) dont chacun est un axiome, une hypothèse, ou résulte des propositions précédentes dans la séquence par une règle d'inférence. La dernière proposition de la séquence est un théorème d'un système formel. La notion de théorème n'est en général pas effective, donc n'existe pas de méthode par laquelle nous pouvons à chaque fois trouver une démonstration d'une proposition donnée ou de déterminer s'il y en a une. Le concept de déduction naturelle est une généralisation de la notion de démonstration. Le théorème est une conséquence syntaxique de toutes les formules bien formées qui la précèdent dans la démonstration. Pour qu'une formule bien formée soit présente dans le cadre d'une démonstration, elle doit être le résultat de l'application d'une règle de l'appareil déductif. Les démonstration formelles sont souvent construits à l'aide d'ordinateurs en tant qu'ass

Source officielle

https://fr.wikipedia.org/wiki/D%C3%A9monstration_formelle

À 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 (6)

Publications associées

Chargement

Personnes associées (1)

Personnes associées

Chargement

Unités associées (1)

Unités associées

Chargement

Concepts associés (22)

La logique — du grec , qui est un terme dérivé de signifiant à la fois « raison », « langage » et « raisonnement » — est, dans une première approche, l'étude de l'inférence, c'est-à-dire des règle

En mathématiques et en logique, un théorème (du grec théorêma, objet digne d'étude) est une assertion qui est démontrée, c'est-à-dire établie comme vraie à partir d'autres assertions déjà démontrées

Un système formel est une modélisation mathématique d'un langage en général spécialisé. Les éléments linguistiques, mots, phrases, discours, etc., sont représentés par des objets finis (entiers, suite

Afficher plus

Concepts associés

Chargement

Cours associés (7)

Cours associés

Chargement

Séances de cours associées (10)

Séances de cours associées

Chargement

Foundations for SCALA

Vincent Cremet

SCALA is an attractive programming language because it is both very expressive and statically strongly typed. This marriage against nature comes at the price of a certain complexity in the language constructs and the static analysis. This complexity makes type safety unclear. The goal of this thesis is to initiate a rigorous and formal process of validation of the SCALA type system. The correctness of a type system can only be established in relation to a formal description of a program execution. The first contribution of this thesis is the definition of a formal semantics for SCALA, by translation in a minimal class-based calculus. SCALA offers two means for expressing type abstraction: type parameters and type members, also called virtual types. Virtual types seem more primitive since they allow to encode type parameters whereas the existence of a reverse encoding is not clear. The soundness of virtual types has been the object of a long debate in the community; they are now commonly believed to be safe, but at this time, there exists no formal argument that would confirm this belief. The second contribution of this thesis is to provide a formal proof of type safety for virtual types.

EPFL2006

Chargement

Symbolic Proofs of Temporal Properties

1994

Chargement

An Equational Theory for Transactions

Vincent Cremet, Rachid Guerraoui, Martin Odersky

Transactions are commonly described as being ACID: All-or-nothing, Consistent, Isolated and Durable. However, although these words convey a powerful intuition, the ACID properties have never been given a precise semantics in a way that disentangles each property from the others. Among the benefits of such a semantics would be the ability to trade-off the value of a property against the cost of its implementation. This paper gives a sound equational semantics for the transaction properties. We define three categories of actions, A-actions, I-actions and D-actions, while we view Consistency as an induction rule that enables us to derive system-wide consistency from local consistency. The three kinds of action can be nested, leading to different forms of transactions, each with a well-defined semantics. Conventional transactions are obtained as ADI-actions. >From the equational semantics we develop a formal proof principle for transactional programs, from which we derive the induction rule for Consistency.

2003

Chargement