Top 20

1 0x00h 701 pts
2 boris39 701 pts
3 neoxquick 682 pts
4 maf-ia 663 pts
5 thefinder 645 pts
6 benito255 609 pts
7 mego 592 pts
8 madbat2 581 pts
9 Mart 554 pts
10 tehron 504 pts
11 Kithyane 503 pts
12 egosum 474 pts
13 plucth 447 pts
14 Undr 416 pts
15 Zeta 416 pts
16 CoYoTe99 416 pts
17 loonies2 412 pts
18 Armavica 411 pts
19 vitalimarrenra 404 pts
20 b0n0n 397 pts

Classement complet

Shoutbox

15 Jul - 8:43 pm

Cool !! Merci beaucoup !!

9 Jul - 11:20 pm

Hello, je regarde ça dès que je peux, probablement demain

9 Jul - 5:54 pm

Bonjour à tous, Je rencontre le même problème que "Foo". Impossible de valider des nouveaux challs, et impossible d'en revalider des anciens... D'avance merci :)

8 Jul - 1:38 pm

Hello. C'est normal que j'arrive pas à valider quoi que ce soit ? La page validation.php renvoie toujours un contenu vide. Même quand j'utilise le code d'exemple donné.

3 Apr - 12:45 pm

Bonjour metatr0n, pas besoin besoin restaurer mon compte précédent puisque j'ai pu revalider les épreuves avec le nouveau :) Si le système de mail ne fonctionne plus, il est probable que l'épreuve "Email (21)" soit également impactée. Au passage je te signale un potentiel problème de précision numérique avec l'épreuve "Polynomial regression (25)" nécessitant plusieurs essais pour valider l'épreuve. Lorsque je vérifie mon polynôme en local (double C++), je respecte pourtant la tolérance de précision. Merci pour les épreuves, je me régale ! :)

26 Mar - 6:14 pm

Bonjour, effectivement notre système de mail a l'air d'être en vrac, si tu veux récupérer ton compte je peux te réinitialiser ton mot de passe à la main

17 Mar - 5:36 pm

Bonjour, l'envoi d'email du système de ré-initialisation de mot de passe semble ne pas marcher (mail orange.fr). J'ai pourtant attendu et vérifié mes spams. J'ai du créer un compte "loonies2" en remplacement de "loonies".

11 Feb - 8:21 pm

Bonjour, oui bien sûr, on peut utiliser n'importe quel langage

9 Feb - 11:30 pm

Bonjours, on peut utiliser python 3 ?

26 Jan - 2:06 pm

Hi, that's right, I'm gonna look into it, thanks

Connexion
Mot de passe oublié

Supportez nousx

Vous aimez µContest ?
Supportez nous en votant (fun et difficulté) pour µContest sur WeChall :)
Si vous ne l'avez pas encore fait, profitez-en pour lier votre compte
Wechall à µContest pour pouvoir voter !

Merci

Liste des épreuves :: Intelligence artificielle :: Formal Systems and Decision Procedures (49)

Résumé

ID : 49
Points : 17
Validations :
Page de l'épreuve
Reporter un bug

Description


Ce challenge est une introduction aux systèmes formels. Il peut être surprenant de le trouver dans la section Intelligence Artificielle, mais ces deux domaines peuvent être intimement liés.
Les systèmes formels sont une modélisation mathématique d'un langage. On peut le voir comme un modèle abstrait d'un système. Par exemple, les langages de programmation sont des systèmes formels. Mais un système formel peut être utilisé pour modéliser le raisonnement mathématique et c'est ce qui nous intéresse ici.

Les systèmes formels en mathématiques sont constitués des éléments suivants :
  • Un ensemble fini de symboles (c.a.d. l'alphabet), qui peuvent être utilisés pour construire des formules (i.e. des chaines finies de symboles).
  • Une grammaire, qui nous dit quelles sont les formules bien formées (abréviées par fbf) construites à partir des symboles de l'alphabet. Une procédure de décision est généralement requise pour décider si une formule donnée est bien formée ou non. Ces fbf peuvent être appelées théorèmes du système.
  • Un ensemble d'axiomes: chaque axiome doit être une fbf.
  • Une ensemble de règles d'inférences.


Le système que nous allons utiliser dans ce challenge est le systèmes TQ que Douglas Hofstadter présente dans son chef-d'oeuvre "Gödel, Escher, Bach: Les brins d'une guirlande éternelle".

Il est défini comme suit :
  • Les symboles sont : t, q et -
  • La grammaire n'est volontairement pas donnée, mais nous verrons cela plus tard.
  • L'ensemble d'axiomes : Si x est une chaine composée uniquement de '-', la chaine xt-qx est un axiome. Vous pouvez constater qu'il y a une infinité d'axiomes dans ce système.
  • L'ensemble des règles d'inférence : Il n'y a qu'une seule règle d'inférence :
    Si x, y et z sont des chaines composées uniquement de '-', et si la chaine xtyqz est un théorème (cad une fbf), alors xty-qzx est également un théorème.


Prenons un exemple.
Avec x = "--", selon la règle de l'axiome,
(1) --t-q-- est un axiome et donc une fbf.
Nous pouvons l'utiliser pour produire de nouvelles chaines avec la règle d'inférence. Ici, x = "--", y = "-" et z = "--". Nous obtenons :
(2) --t--q----
Nous avons maintenant une fbf qui n'est pas un axiome (cad un théorème). Mais c'est super, nous pouvons l'utiliser pour produire un nouveau théorème avec la règle d'inférence :
(3) --t---q------
etc.

Maintenant vous comprenez que les axiomes sont les chaines de base, à partir desquelles nous allons "produire" les autres chaines (les théorèmes), qui seront des chaines bien formées de notre système formel. Nous pouvons également imaginer que certaines chaines ne seront jamais produites, peu importe l'axiome de départ qu'on choisit pour appliquer notre règle d'inférence. C'est exactement l'intérêt de ce challenge : Comment déterminer automatiquement, en un temps fini, si une chaine donnée est un théorème de notre système ou pas ? (Vous voyez le rapport avec l'intelligence artificielle maintenant... ?). De telles procédures automatiques sont appelées Procédure de Décision, et peuvent même ne pas exister.
Rassurez vous, dans ce cas, elle existe, il en existe même plusieurs.

Vous allez recevoir 15 chaines et votre rôle va être de déterminer lesquelles d'entre elles sont des théorèmes, c'est à dire celles qui peuvent être produites à partir des axiomes en appliquant la règle d'inférence.

Les chaines sont données dans les variables string1, string2, ..., string15.
Vous allez envoyer vos réponses dans des variables séparées. Si string1 est un théorème, alors vous devrez renvoyer theorm1=1, theorm1=0 sinon.

Par exemple, si
string7 = --t---q------
Alors vous devez retourner :
theorem7 = 1

Mais si
string7 = --t--q--
Alors vous devez retourner :
theorem7 = 0 (croyez moi ;) ).

Indice : Il y a deux manières de résoudre ce challenge, la manière forte, et la manière intelligente...
Note 1: Une chaine de '-' peut être vide.
Note 2: Les axiomes comptent en tant que théorèmes.

Variables


Nom Type Description
Variables à récupérer
string1Chaîne de caractèreschar*La première chaine dont vous devez determiner si c'est un théorème de TQ ou non
string2Chaîne de caractèreschar*La 2e chaine dont vous devez determiner si c'est un théorème de TQ ou non
...Chaîne de caractèreschar*
string15Chaîne de caractèreschar*La 15e chaine dont vous devez determiner si c'est un théorème de TQ ou non
Variables à renvoyer
theorem1EntierintVaut 1 si string1 est un théorème de TQ, 0 sinon.
theorem2EntierintVaut 1 si string2 est un théorème de TQ, 0 sinon.
...Entierint
theorem15EntierintVaut 1 si string15 est un théorème de TQ, 0 sinon.