Top 20

1 0x00h 696 pts
2 boris39 696 pts
3 neoxquick 677 pts
4 maf-ia 659 pts
5 thefinder 640 pts
6 benito255 605 pts
7 nikokks 598 pts
8 mego 589 pts
9 madbat2 580 pts
10 eax 568 pts
11 plucth 561 pts
12 Mart 550 pts
13 Stupefy 530 pts
14 tehron 503 pts
15 Kithyane 498 pts
16 egosum 471 pts
17 malose 428 pts
18 CoYoTe99 415 pts
19 Undr 413 pts
20 Zeta 413 pts

Classement complet

Shoutbox

24 Aug - 7:10 pm

@rostale, en effet l'épreuve 21 ne fonctionne plus depuis un moment, pour l'instant on a pas prévu de temps pour la réparer je pense qu'on va finir par la supprimer tout simplement. @nikokks, ok je t'envoie un mail

22 Aug - 11:40 pm

Salut Metatr0n. pourrait on avoir une discussion en MP. J'imagine que tu as mon mail. Ce serait pour discuter de microcontest en general.

28 Jul - 10:38 pm

Pouvez-vous vérifier l'épreuve Email (21) ? En effet, je ne reçois pas d'email de la part du site. Merci

28 Jul - 7:29 pm

Bonjour et merci. Cependant, j'ai résolu le challenge qui me posait pb, donc plus rien à demander... pour l'instant.

28 Jul - 1:48 pm

Ça devrait être réparé maintenant

28 Jul - 12:04 pm

Bonjour, effectivement j'ai le même message d'erreur, on va investiguer merci d'avoir rapporté le soucis

23 Jul - 6:49 pm

Ca veut dire quoi ce message lorsque je veux poster sur le forum ? Votre liste étant trop longue pour être analysée, veuillez la réduire s'il vous plaît !

25 May - 12:07 pm

NGXKGTFWPGODKPGPFQTOKIIVNCJCYVNIWIPVTIFQYDNCKVYPW

9 Apr - 2:10 pm

Yeah this email challenge is a pain in the ***. Sorry about that, we might even remove it in the future, i will see if we find time to fix it

2 Apr - 7:03 am

The Email challenge (#21) appears to be broken again. No mail is being received. Tried with multiple mail services to no avail.

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.