Engineer's Book

Engineers – Telecoms – Physics – Teaching – Surveying

Formal Méthod – Complex Method to Manage … Complexity ?

Written By: Jean-Paul Cipria - Déc• 09•17

The Formal Method claims to reduct systems logical errors number. But do we succeed to use, logically, the Formal Method ? It is a very smart paradox. Is’nt it ?

We are sorry. Those following Annexes from PhD Thesis are in French language. Some denounced ideology and author irony are typicaly … local French. Let’s try to understand French hidden meanings. Ideas are existing and relationships must be described and meaning can be detected. Is it an ontology ? It is a good exercice for us !

.

Created :2017-12-09 18:36:29. – Modified : 2017-12-29 21:32:37.

.

Very Difficult ! PhD Level.

Very Difficult ! PhD Level


Expériences En Construction

Experiment is being drawn up

Abstracts : Here we get read the methods theorical first lines to « see » how some engineers can’t understand very simple concepts by changing formal description forms from difficulties to complexities objects. Then an engineer can loose his intelligence by page 2 [SHEERAN-STALMARCK-1998] references when he can’t remember differences between « implication » and « deduction » ? And what about the following ? He discovered that some logical rules are redundant when he knows about thirty years to contract it on the minimal information quantity by Morgan equivalent theorem method but only in boolean logical implication ?

Unlike the reference document is it possible to « contract » as minimal information by Maximum Entropy Method [CIPRIA-M.E.M.-2016] from for exemple 100 000 rules to a set of 100 or 10 only ones ? Then we will avoid to have to test or read all redundant branches of a very big logical tree ? Thus processor time will be dedicated to find the « essentielle moelle » rather than doing « brute forces » ? Will we spend beginning processor time not to calculate some ways or pathes with dicotomy methods but trying to modelize the minimum package equations before to throw it to calculation methods ?

Méthode Formelle : les notions de départ ?

Et meeeeeeeerde !

Il s’agit de remplacer un ensemble de règles logiques, qui deviennent surabondantes, qui overclokent le temps CPU, qui overstackent les mémoires dynamiques, qui forgettent certaines exceptions, qui ne handcheckent plus, par une méthode formelle qui en définissant tout de façon conceptuelle perd pied avec la réalité ? En partant de systèmes à la Hilbert nous effectuons quelques prédicats et de calculs de séquents mais qu’en est-il de la théorie des modèles ? Et réciproquement, en inférant, en prenant comme exemple tous les exemples de la réalité, elle ne « tombe » pas sur l’exception qui ne tardera pas à se présenter selon la célèbre loi de l’emmerdement maximum ?

Pourquoi une implication n’est pas un OU inclusif ?

  • To follow …. 16/12/2017

Est-ce qu’un Railway Interlocking est un OU exclusif ?

Partie privée
Sujet « chaud » du moment par hasard (15/12/2017). Sujet auto-bloqué par l’auteur jusqu’à refroidissement des esprits. Constatations confidentielles.

Fin de partie privée.

.

Qu’elle est la différence entre une implication et une déduction ?

L’un « contient » l’autre ?

En fait il convient de « monter » une définition vers un concept supérieur. La déduction « contient » une implication dans laquelle l’élément de départ et celui d’arrivée sont préalablement définis. Tout comme monsieur Jourdin vous typez vos variables : a integer, b boolean; en programmation C en désignant dans quel espace vont « évoluer » vos variables.

En méthode formelle vous désignez préalablement votre « Cause » a, votre « Cause Implication Conséquence » et votre « Conséquence » b.

  • A,~ A\rightarrow B, ~B

C’est lourd ! Mais nous faisons cela tous les jours. Ceci évite ce que l’on fait toutes les minutes, c’est à dire d’ajouter 41 à 42 ce qui fait 83 ? alors que cela devrait faire « AB » qui est égal à « 4142 » en deux octets ! Bug ! Warning ! Pour les professionnels du compilateur. Si vous avez de la chance !

En mathématique c’est aussi ce que nous faisons :

  • \forall A \in A_i ~\exists B \in B_i~ a \Rightarrow B=f(A)
  • A \vdash B De A je déduis B ?

Ce type de contraction du concept l’implication si … alors \Rightarrow vers la déduction « donc » \vdash serait puissante si elle était utilisée comme nous le présentons sur les deux lignes précédentes. MALHEUREUSEMENT CE N’EST PAS LE CAS. Le concept « supérieur » \vdash s’écrit avec plus de lettres que celui du … inférieur \forall A \in A_i ~\exists B \in -i~ a \Rightarrow B=f(A) . Si nous pouvons nous exprimer ainsi ?

Ainsi un ET logique booléen s s’écrit  :

  • s=A \wedge B

Et le concept S « au-dessus » s’écrit :

  • S=\begin{array}{cc}\dfrac{A \wedge B}{A}\\B\end{array}

Il y a dans ce cas simple une tautologie. C’est à dire que ce qui est au dessus de la « fraction » ou plutôt du signe d’équivalence est la même chose que A superposé à B et qu’il faut que A soit vrai et que B soit vrai pour que la proposition S soit vraie.

Ou astuce, nous faisons la proposition sur la solution S puis nous fixons A et nous déduisons quel est l’état de B. Nous avons la solution et nous étudions tous les états possibles des variables pour la rendre vraie.

Cette première lecture par un ingénieur dont le background est important apporte un tas de confusions que nous venons d’expliquer. Pourquoi énoncer tant de tautologies toto=toto ? Cette première phase des « explications » dites préliminaires  dans le document cité en référence [SHEERAN-STALMARCK-1998] apporte plus de malentendus que d’aborder directement un exemple plus complexe. Les auteurs « nous font tomber dans le panneau ». Nous cherchons beaucoup plus loin une conception mathématique que « porteraient » ces équations, qui n’existe pas ! Ainsi à la lecture des premières pages nous pensions naïvement que les auteurs « étendaient » le concept :

Contraction ou extension des concepts ?

Cette façon d’écrire est, en quelque sorte, la réciproque d’une contraction à la Einstein du style e^i.u_j qui est une somme sur tous les éléments e et u ? Et qui est une « contraction » du signe somme en plusieurs dimensions. Tout le monde n’est pas Einstein ? Plus facile à lire mais plus difficile à concevoir.

C’est à dire, qu’en méthode formelle, classique, plus nous conceptualisons et … plus c’est long à écrire. Ou autrement dit  : « Plus l’objet à décrire est difficile et plus la méthode formelle devient … complexe ? »

Bref, nous venons de décrire simplement ce qu’est une ontologie dont la définition données par tous les sites qui n’y comprennent rien : « étude de l’être en tant qu’être » représente une absurdité ? Pourquoi ? Il s’agit d’étudier les éléments de la logique soit A est vrai et en plus il existe. Ce qui commence à être une ontologie quand nous précisons que si A implique B et que B est vrai. Nous venons de définir l’existence des êtres mathématiques ou physiques A et B ainsi que la règle ou la syntaxe qui les lie. Ceci commence à donner du « sens » à l’existence de A, de B et d’une liaison entre eux deux. Ce n’est pas bien difficile. Enchâsser 20 pages de doctorat sur cette petite chose est malheureusement chose courante. Pour ceux bernés par la fausse définition courante qui se sert d’une étymologie hors contexte pour déblatérer une tautologie. Des preuves ? 😉

Industrie de la complexité ?

Ce qui est un excellent « passage » mathématique du type « Ingénieur » au type « Comptable » sur un sujet sur lequel nous avons beaucoup travaillés.

En effet l’industrie « possède » beaucoup de méthode(s) comptable(s). Nous hésitons à mettre au pluriel ? L’industrie est organisée. Elle sait faire des tables, des tableurs, des classements et des moteurs pour s’y retrouver. Mais elle ne sait pas, en général, résoudre une équation différentielle. En ce cas l’industrie délègue à un … technicien qui « vaut » la moitié d’un commercial. Elle croit faire des économies en gérant plutôt qu’en réfléchissant. Ce qui est le lot des organisations pyramidales ou en balai.

Donc :

  • Rigidite_{Entreprise} \vdash Flexibilite _{Salaries}     CQFD 😉

Et cette déduction n’est pas réciproque ? Trouvez des contre-exemples !

.

To follow …. 16/12/2017

Comprendre une méthode de compréhension ?

En fait, comme d’habitude, il faut sauter, biffer, oublier, forgetter, goto to, les premières pages d’introduction mathématiques dites « simples » et aller plus loin aux pages dites « difficiles ». Et là vous comprenez assez facilement les choses dites difficiles qui vous font comprendre les choses simples … du début ! En sémantique nous appelons cela un « begin to and from the end ». Copyright JP Cipria. 😉

Donc les savants nous expliquent, le « Monsieur te dit », « 2.5 The Intrinsic Redundancy of Cut-Free Proofs » que si tu déroules ta logique, que tu l’exprimes en booléen, en prédicats ou en séquents, tu vas obtenir une redondance dans ta vérification. Tu vas trouver dans une branche de ton arbre de vérification de gauche exactement une même branche un peu plus bas sur la partie de droite. Toute l’astuce est de détecter au deuxième passage de droite le calcul déjà effectué sur l’arbre de gauche pour ne pas ? le refaire ! Merci Monsieur. Encore fallait-il qu’ils nous le disent. C’est fait. Nous venons de diviser le nombre de calculs par environ deux dans le cas précisé par les auteurs.

To follow …. 17/12/2017.

Références

  • [SHEERAN-STALMARCK-1998] : « A Tutorial on Stalmarck’s Proof Procedure for Propositional Logic. » Page 82 à 98
    .

    • Type Article de revue
      Auteur Mary SHEERAN
      Auteur Gunnar STALMARCK
      Collection Lecture Notes in Computer Science
      Numéro 1522
      Pages 17
      Publication Edited by G. Goos, J. Hartmanis and J. van Leeuwen
      Date 1998
      Consulté le 12/09/2017 à 02:00:00
      Langue English
      Résumé Abstract. We explain Stalmarck’s proof procedure for classical propositional logic. The method is implemented in a commercial tool that has been used successfully in real industrial verication projects. Here, we present the proof system underlying the method, and motivate the various design decisions that have resulted in a system that copes well with the large formulas encountered in industrial-scale veri⬚cation. We also discuss possible applications in Computer Aided Design of electronic circuits.
      Date d’ajout 09/12/2017 à 13:52:37
      Modifié le 09/12/2017 à 14:03:37

      Pièces jointes

    • STALMARCK-SHEERAN-Formal Methods in Computer-Aided Design-1998.pdf

Jean-Paul Cipria

  • [CIPRIA-M.E.M.-2016] : Jean-Paul Cipria, « Maximum Entropy Method – Notions » – 2016

Maximum Entropy Method – 1 – Notions

Acronymes

  • KBES: Knowledge Base Expert System : Lisp, Prolog.

.

09/12/2017
Jean-Paul Cipria

You can follow any responses to this entry through the RSS 2.0 feed. You can skip to the end and leave a response. Pinging is currently not allowed.

Laisser un commentaire

Votre adresse de messagerie ne sera pas publiée. Les champs obligatoires sont indiqués avec *

Anti-Spam Quiz: