Top 20

1 0x00h 701 pts
2 boris39 701 pts
3 neoxquick 682 pts
4 maf-ia 663 pts
5 thefinder 644 pts
6 benito255 608 pts
7 mego 591 pts
8 madbat2 581 pts
9 Mart 554 pts
10 Stupefy 533 pts
11 tehron 504 pts
12 Kithyane 502 pts
13 plucth 480 pts
14 egosum 473 pts
15 CoYoTe99 416 pts
16 Undr 415 pts
17 Zeta 415 pts
18 loonies2 411 pts
19 Armavica 410 pts
20 vitalimarrenra 403 pts

Classement complet

Shoutbox

28 Feb - 10:35 am

Yes we fixed it

27 Feb - 10:00 pm

Thank you, just validated contest22. The solution checker seems to have been fixed.

27 Feb - 8:40 am

Yes several solutions are accepted of course. I will check one of your answers

26 Feb - 7:51 pm

No 500 error, but the solutions I'm submitting can be verified to be correct. It can't be that only one configuration is accepted, right? - as there are multiple correct configurations for each problem.

26 Feb - 5:54 pm

contest 22 is not concerned by the issue I found, and seems to be working (I suppose you don't have 500 error on this one ?). Your solutions are indeed rejected, but I did not check them yet

26 Feb - 3:25 pm

The validation for contest 22 also seems to be wrong (it's not accepting solutions that are clearly correct). I submitted bug report yesterday.

26 Feb - 9:59 am

Ok I fixed the issue It is higly possible that other challenges are impacted, so don't hesitate to tell meif you encounter this again. Thank you for reporting

26 Feb - 9:28 am

No I was wrong, it is server side. It looks like the validation script does not work anymore, for some reason I am trying to understand. I will keep you informed when it's fixed

26 Feb - 9:22 am

Actually I don't see any attempt from you in the logs. I see your variable request, but I don't see any solution sent. I would incriminate the python lib since nobody ever complained not beeing able to validate this chal, but it can be server side.

25 Feb - 10:43 pm

When I submit any solution to contest45 from Python library, there is an HTTP 500 Error. Must be a server-side parsing error?

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.