The 2nd International Conference on Algorithms for Computational Biology (AlCoB 2015) / go to DF in August -- Vleeptron SWEARS you'll love the food if Plaza Garibaldi's still there / do not yell "Taxi!" in front of your hotel / if you're in Holy Orders, wear your vestments, it's legal now

Click image and postage meter to enlarge.


The 2nd International Conference on 
Algorithms  for Computational Biology
(AlCoB 2015) 
invites authors to submit work in progress for presentation.
AlCoB 2015 will be held in Mexico City on August 4-6, 2015. See

http://grammars.grlmc.com/alcob2015/

Presentations are intended to enhance informal interactions with conference participants, at the same time permitting in-depth discussion.

TOPICS

Authors can submit presentations describing novel work in progress on any of the topics within the scope of the conference. They do not need to contain final results, but research that may lead to future interesting developments
is welcome.

KEY DATES

Submission deadline: June 26, 2015
Notification of acceptance or rejection: 7 days after submission

SUBMISSION

Please submit a .pdf abstract through:

https://www.easychair.org/conferences/?conf=alcob2015

It should contain the title, author(s) and affiliation, and should not exceed 500 words.

PRESENTATION

Each presentation will be allocated 15 minutes in the programme.

PUBLICATION

The presented work will not appear in the LNCS/LNBI proceedings volume of AlCoB 2015. However, it will be eligible for submission to the post-conference Journal of Computational Biology special issue.

REGISTRATION

Authors of work in progress have to register to the conference. They will pay a reduced fare. This comprises access to all sessions, one copy of the proceedings volume, coffee breaks and lunches.


---
 
Este mensaje no contiene virus ni malware porque la protección de avast! Antivirus está activa.
http://www.avast.com

[Coq-Club] formalisation de la logique propositionnelle / introduction to conversational Martian

Bonjour

J'espère que vous êtes conscient que l'enseignant qui vous a donné ce projet a toutes les chances de lire cette mailing liste, et qu'il n'est pas évident qu'il considère que faire corriger/compléter votre
réponse soit exactement le travail qu'il attendait de vous.

J'espère aussi que vous penserez, avant de rendre votre projet, à supprimer le nom de votre camarade Samuel Besset, et à le remplacer
par le votre. Cela risquerait de d'éveiller des soupçons de triche. Ce serait malheureux.

Cordialement,

Alexandre Pilkiewicz

Le 21 avril 2011 11:46, aymen bouslama a écrit:

bonjour,
 

est ce que vous pouvez me dire si c'est juste ce que j'ai fais pour résoudre le problème suivant?
 

Construire un type inductif a deux constructeurs permettant de mod eliser le  fragment implicatif de la logique propositionnelle. Les termes seront soit des  variables, not ees a, b, c, etc. (prises dans un ensemble V ), soit une implication entre deux termes.

On pourra utiliser la biblioth eque String de Coq pour g erer les noms des propositions.

Interpretation On propose de repr esenter une valuation par une liste de paires (variable,bool een).

Definition valuation := list (string * bool).

Ecrire une fonction list assoc qui, etant donn ee une variable  propositionnelle et une valuation V donne la valeur de la variable dans la valuation.

Ex : si
 V=[("x",true);("y", false)] list_assoc V y=false.

 Ecrire une fonction d'interpr etation qui, etant donn e une formule F et  une valuation I, calcule si I satisfait F , i.e. I(F ) = true.

Tables de v erit e Programmer une fonction qui prend en argument un terme du calcul propositionnel et calcule s'il s'agit d'une tautologie ou non en utilisant une table de v erit e.

Indication : on pourra enum erer toutes les valuations possibles. Il su ra ensuite de tester que la formule est satisfaite pour toutes ces valuations. On pourra pour cela utiliser les fonctions d'ordre sup erieurs sur les listes (par exemple forallb). Pour l'implication (2 variables), le nombre de cas a etudier pour d eterminer si on a a faire a une tautologie est 4.

 Utiliser votre fonction pour v eri er que les termes suivants sont bien des tautologies.

 { Pierce : ((A - B) -A) -A
 { S : F -(G - F )
 { K : (F - (G - H)) - ((F - G) - (F - H))
 -------------------------------

 (*---------------------------------------------------------------------------------*)
 (*------------------------------ PROJET COQ M1 ILC
 --------------------------------*)
 (*------------------------------ BESSET SAMUEL
 --------------------------------*)
 (*---------------------------------------------------------------------------------*)
 Require Export List.
 Require Export String.
 Require Export Bool.
 Open Local Scope char_scope.
 (*---------------------------------------------------------------------------------*)
 (* Formaliser la syntaxe et sémantique et modéliser un système de déduction
 *)
 (*---------------------------------------------------------------------------------*)

 (*---------------------------------------------------------------------------------*)
 (*
 SYNTAXE *)
 (*---------------------------------------------------------------------------------*)

 (* Définition inductive du type : form *)
 Inductive form : Set :=
 | p : string - form (* proposition *)
 | i : form - form - form (* implication *)
 | e : form - form - form (* ET logique *)
 | o : form - form - form (* OU logique *)
 .
 (*---------------------------------------------------------------------------------*)
 (*
 SEMANTIQUE *)
 (*---------------------------------------------------------------------------------*)

 (* Définition de la valuation *)
 Definition valuation := list (string * bool).

 (* Définition de la fonction : list_assoc *)
 Fixpoint list_assoc a (v:valuation) : bool :=
 match v with
 | nil = false
 | (x,b) :: l =
 if string_dec x a then b
 else list_assoc a l
 end.

 (* Définition de la fonction : interpretation *)
 Fixpoint interpretation form (v:valuation) : bool :=
 match form with
 | p s1 = list_assoc s1 v
 | i form1 form2 = (orb (negb (interpretation form1 v)) (interpretation
 form2 v))
 | e form1 form2 = (andb (interpretation form1 v) (interpretation form2
 v))
 | o form1 form2 = (orb (interpretation form1 v) (interpretation form2 v))
 end.

 (*---------------------------------------------------------------------------------*)
 (* TEST -
 SEMANTIQUE *)
 (*---------------------------------------------------------------------------------*)

 (* Tests des définitions précédentes : *)
 Definition a := (String "A" EmptyString).
 Definition b := (String "B" EmptyString).
 Definition val := (a,true)::(b,false)::nil.

 Eval compute in (interpretation (p a) val). (* doit rendre : true *)
 Eval compute in (interpretation (p b) val). (* doit rendre : false *)
 après avez vous une idée pour la suite?
 Syst eme formel
 On rappelle les r egles de la d eduction naturelle : comme elim et intro
 On d eclare un contexte (comme ) comme une liste de formules.
 Definition context := list formule.
 1. Mod eliser le syst eme formel pr ec edent a travers un type inductif de la forme :
 Inductive prouvable : context - formule - Prop := ...
 2. Prouver ensuite le th eor eme A - A dans ce syst eme.
3. Faire de m^eme avec les th eor emes S et K de la section pr ec edente.
4. On va maintenant s'int eresser a la preuve de la correction de ce systeme formel.
(a) D e nir un pr edicat consequence_l qui prend en argument un contexte et une  formule F et indique si F est cons equence s emantique de .
(b) Prouver le th eor eme suivant :
Lemma correctness : forall P G,
provable G P - consequence_l G P.

 merci
 Cordialement

wtf moment du jour, all guesses and comments welcome

Hi Gyesik and Matthieu,

Consider the following proof for your goal:

Theorem le_Pfact: forall x:nat, exists y, Pfact x y.
Proof.
fix circ 1.
intro.
destruct x.
exists 1.
constructor.
destruct x.
exists 1.
constructor.
pose proof (circ x) as H.
destruct H. (* existential var becomes x0 *)
exists (x * x0).
constructor.
assumption.
Save.

I find the above style of inductive proof much easier. Of course, the hypothesis "circ" must be applied in a well-founded way. However, there's no need to have an adequate induction principle readily available (or even bother to know what that induction principle should be).

Hope this helps,

Razvan

Matthieu Sozeau wrote:
{
{ Le 27 janv. 10 à 10:57, Gyesik Lee a écrit :
{
{{ Hi,
{}
} Hi Gyesik,
}
{{ as in the following case, an induction principle provided by Coq is sometimes not strong enough:
}}
{{ (A modified version of the example in Section 8.4.1.1 of CoqArt book.)
{{ ===================
{{ Open Scope nat_scope.
}}
{{ Inductive Pfact : nat -> nat -> Prop :=
{{ | Pfact0 : Pfact 0 1
{{ | Pfact1 : Pfact 1 1
{{ | Pfact2 : forall n v : nat, Pfact n v -> Pfact (S (S n)) (n * v).
}}
{{ Axiom lt_wf : well_founded lt.
}}
{{ Theorem le_Pfact : forall x : nat, exists y, Pfact x y.
{{ induction x.
{{ (* then the induction hypothesis is not strong enough*)
{{ Abort.
}}
{{ induction x using lt_wf.
{{ (* then the claim can be easily proved. *)
}}
{{ ===================
}}
{{ I am wondering if Coq provides a kind of mechanism producing the induction principle reflecting the well-foundedness of the canonically definable structural orderings on inductive types.
}
} My soon-to-be-released Equations [1] plugin has ML code to generate this order on any non-impredicative, computational inductive family (ie. most datatypes). You can derive both the subterm relation (actually the transitive closure of the direct subterm relation) and its wellfoundedness proof and a [Below] predicate that can be used to recurse and get a tuple
} of all the possible recursive calls in the context. You don't need to worry about guardness checks anymore if you use any of these, but you have to provide proofs that recursive arguments decrease in the first case or find your way in a tuple in the second case. This is partially automatable though.
}
} }}
}
} Require Import Equations.
}
} Open Scope nat_scope.
}
} Inductive Pfact : nat -> nat -> Prop :=
} | Pfact0 : Pfact 0 1
} | Pfact1 : Pfact 1 1
} | Pfact2 : forall n v : nat, Pfact n v -> Pfact (S (S n)) (n * v).
}
} Derive Subterm for nat.
}
} Theorem le_Pfact : forall x : nat, exists y, Pfact x y.
} apply FixWf; intros.
} destruct x. econstructor; constructor.
} destruct x. econstructor. constructor.
} destruct (H x). solve_rec.
} exists (x * x0). constructor; auto.
} Qed.
}
} Derive Below for nat.
}
} Definition rec_nat (P : nat -> Type) (step : Π n, Below_nat P n -> P
} n) n : P n :=
} step n (below_nat P step n).
}
} Theorem le_Pfact' : forall x : nat, exists y, Pfact x y.
} induction x using rec_nat.
} destruct x. econstructor; constructor.
} destruct x. econstructor. constructor.
} simpl in X. destruct_conjs.
} exists (x * e0). constructor; auto.
} Qed.
}
} }}
}
} [1] http://mattam.org/research/coq/equations.en.html
}
} -- Matthieu