Top 20

1 0x00h 686 pts
2 boris39 686 pts
3 thefinder 686 pts
4 neoxquick 667 pts
5 maf-ia 649 pts
6 eax 648 pts
7 nikokks 605 pts
8 benito255 596 pts
9 mego 579 pts
10 madbat2 570 pts
11 plucth 553 pts
12 Mart 540 pts
13 rostale 540 pts
14 Stupefy 521 pts
15 tehron 505 pts
16 LouisJ 492 pts
17 Kithyane 489 pts
18 egosum 464 pts
19 malose 419 pts
20 CoYoTe99 408 pts

Full ranking


8 Oct - 10:01 am

Salut nikokks Ce problème n'est pas évident en effet. Une manière de faire est de trouver les formes les plus simples, et de les "effacer" de l'image avant de chercher les formes plus complexes ;)

4 Oct - 11:56 am

Salut a tous =) , je bug sur le problème 28 (forme analysis). Quelqu'un aurait il une piste ?

29 Sep - 5:38 pm

Coucou oui, tu peux m'envoyer un mail si tu veux. Le plus simple, ce serait d'avoir un package pour python 3. J'ai essayé et ça n'a pas marché!

17 Sep - 11:51 am

Salut thefinder, ça faisait longtemps ! Oula ça en fait des problèmes :'( Le premier challenge ? La somme de deux nombres ?

23 Jul - 2:13 am

Coucou, j'ai essayé de reprendre avec python. J'ai plusieurs soucis. 1) Il faut rajouter headers={'Content-Type': 'application/x-www-form-urlencoded'} avec un requests.session(). 2) Je n'ai pas réponse du serveur si je soumet une réponse au premier challenge. J'essaye finir en python les 3 dernières épreuves qui me reste. :)

6 Nov - 8:17 am

Bonjour, un léger problème sur l'épreuve 10 : Une fois réussie, le champ "points earned" indique 72 au lieu de 7 En revanche sur le site le nombre de points comptabilisés est bien 7 Merci pour ce site génial !

21 Oct - 9:48 pm

Équation du challenge 52 corrigée, merci

16 Oct - 8:43 am

Bonjour, il y a aussi un problème d'affichage "invalid equation" dans le challenge 52. Merci

14 Oct - 8:57 pm

Barbapapou l'équation du challenge 29 a été corrigée

4 Oct - 10:30 am

Bonjour, il y a un problème avec l'affichage d'une équation dans le challenge 29

Password forgotten

Support usx

You like µContest ?
Support us by voting (fun and difficulty) for µContest on WeChall :)
If you have not already, take the opportunity to link your Wechall
account to µContest in order to be able to vote !

Thank you

Contests list :: AI :: Formal Systems and Decision Procedures (49)


ID : 49
Points : 17
Validations :
Challenge page
Report a bug


This challenge is an introduction to the formal systems. It might be surprising to see it in the Artificial Intelligence section, but these two fields can be intimately linked.
The formal systems are basically a mathematical modelisation of a language. This is, in a way, an abstract model of a system. For example, programming languages are formal systems. But a formal system can be used to model the mathematical reasoning and that is what we are interested in here.

Formal systems in mathematics consist of the following elements:
  • A finite set of symbols (i.e. the alphabet), that can be used for constructing formulas (i.e. finite strings of symbols).
  • A grammar, which tells how well-formed formulas (abbreviated wff) are constructed out of the symbols in the alphabet. It is usually required that there be a decision procedure for deciding whether a formula is well formed or not. These wff can be called the theorems of the system.
  • A set of axioms: each axiom must be a wff.
  • A set of inference rules.

The system we are going to use in this challange is the TQ system that Douglas Hofstadter presents in his masterpiece : "Gödel, Escher, Bach: An Eternal Golden Braid".

It is defined as follow :
  • The symbols are : t, q and -
  • The grammar is volontarily not given, but more about that later.
  • The axiom set : If x is a string composed only by '-', the string xf-qx is an axiom. You can see that there is an infinite number of axioms in this system.
  • The inference rules set : There is only one inference rule : If x, y and z are strings composed only by '-', and if the string xtyqz is a theorem (ie a wff), then xty-qzx is also a theorm.

Let's take an example.
With x = "--", according to the axiom rule,
(1) --t-q-- is an axiom and therefor, a wff.
We can use it to produce new strings with the inference rule. Here, x = "--", y = "-" and z = "--". We obtain :
(2) --t--q----
We have now a wff that is not an axiom (ie a theorem). But that's great, we can use it to produce a new theorm with the inference rule :
(3) --t---q------

Now you understand that the axioms are the basic strings from which we are going to "produce" other strings (the theorems) that will be well formed formulas of our formal system. We can also imagine that some strings won't be ever produced, whatever the axiom we choose to apply our inference rule. This is exactly the point of this challenge : how to automatically determine, in a finite time, if a given string is a theorem of our system or not ? (see the link with the artificial intelligence now... ?). Such automatic procedure is called Decision Procedure, and may not even exist.
But don't worry, in this case, it exists and is quite simple (actually several exist).

You are going to be given 15 strings and your role will be to determine which ones of them are theorems, ie the ones that can be produced from the axioms by applying the inference rule.

The strings are given in the variable string1, string2, ..., string15.
You will send your answers in separate variables. If string1 is a theorem, then you will send theorm1=1, theorm1=0 otherwise.

For example, if
string7 = --t---q------
then you should return :
theorem7 = 1

But if
string7 = --t--q--
then you should return :
theorem7 = 0 (trust me ;) ).

Hint : There is two ways to solve this challenge, the bruteforce way, and the smart way...
Note 1: A string composed by '-' can be empty.
Note 2: An axiom counts as a theorem.


Name Type Description
Variables to get
string1Stringchar*The first string for which you have to determine whether it is a theorem of TQ or not
string2Stringchar*The 2nd string for which you have to determine whether it is a theorem of TQ or not
string15Stringchar*The 15th string for which you have to determine whether it is a theorem of TQ or not
Variables to send back
theorem1IntegerintIs 1 if string1 is a theorem of TQ, 0 otherwise
theorem2IntegerintIs 1 if string2 is a theorem of TQ, 0 otherwise
theorem15IntegerintIs 1 if string15 is a theorem of TQ, 0 otherwise