Top 20

1 0x00h 697 pts
2 boris39 697 pts
3 neoxquick 678 pts
4 maf-ia 659 pts
5 thefinder 641 pts
6 benito255 605 pts
7 mego 588 pts
8 madbat2 577 pts
9 Mart 550 pts
10 tehron 500 pts
11 Kithyane 500 pts
12 egosum 470 pts
13 plucth 444 pts
14 Zeta 414 pts
15 Undr 412 pts
16 CoYoTe99 412 pts
17 Armavica 407 pts
18 vitalimarrenra 401 pts
19 b0n0n 394 pts
20 nurfed 382 pts

Classement complet

Shoutbox

20 Aug - 6:04 am

Hi b0n0n, this chall does not appear to be broken sorry. What is your problem ?

14 Aug - 11:22 pm

Multiplication of two (big) numbers (40) is broken, anyone plz fix it?

15 Feb - 3:58 am

En vérité je reconnais que c'est surtout moi qui ait des soucis majeurs ... je reçois le mail là, puis pour la compression ça doit être un problème stupide de mon côté

6 Feb - 8:09 pm

Pour le chall sur les mail je confirme, on a toujours galéré à le faire marcher pour tout le monde et on a fini par abandonner ^^. Par contre pour DC 2, je suis étonné, personne n'a jamais reporté de problème. N'hésite pas à poster ta question sur le forum j'y répondrai :)

6 Feb - 10:16 am

Par exemple le challenge réseau sur le mail ne fonctionne pour pas moi je ne reçois rien. Après c'est surtout des soucis de mon côté, je suis sur data compression 2 et bien que mon algo soit, je crois, correct, je ne peux pas valider parce que je gère mal les caractères spéciaux, je voulais d'ailleurs poster dans le forum pour demander la chaîne finale de l'exemple

6 Feb - 9:22 am

Merci :) Il y aurait encore beaucoup à faire mais bon. Genre normaliser les données des épreuves en json, permettre aux membres de pouvoir "affronter" les programmes des autres (section Arena), rendre le site plus intuitif, etc etc... A quels problèmes mineurs penses tu ?

5 Feb - 4:52 am

très très propre votre entreprise, quelques soucis mineurs mais dans l'ensemble vos challenges sont super à faire, merci !!

2 Feb - 10:09 am

Il y a malgré tout toujours une petite activité régulière, ça fait plaisir

29 Jan - 10:08 am

Et ouais ! Perso je viens toujours tous les jours, c'est ma petite routine quotidienne :)

29 Jan - 12:24 am

y'a encore des gens ici ?

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.