@ -14,7 +14,7 @@ Une **étoile** est une séquence de rayons qu'on peut considérer comme une cla
```
[r1, ..., rn]
```
Les étoiles sont capables d'interagir ensemble le long de rayons connectables par la règle de résolution de Robinson. Par exemple : `[X, -f(X)]` et `[+f(a)]` connectés ensemble le long du symbole `f` donne `[a]`.
Les étoiles sont capables d'interagir ensemble le long de rayons connectables par la règle de résolution de Robinson. Par exemple : `[X, -f(X)]` et `[+f(a)]` connectés ensemble le long du symbole `f` donne `[a]`. On appelle cette opération une étape de **fusion**. On peut voir cela comme une résolution de contraintes entre termes.
Une **constellation** est une union disjointe d'étoiles séparées par le symbole `+`. On peut considérer que les constellations sont des sortes de programmes dans ce modèle. Une constellation est délimitée par des accolades.
@ -26,9 +26,10 @@ Ce que l'on cherche à exécuter n'est pas une constellation mais un **espace d'
```
<constellation> |- <constellation>
```
La constellation à gauche de `|-` est la *constellation de référence* et la constellation de droite est *l'espace d'interaction*. L'idée de l'exécution est que les étoiles de l'espace d'interaction va se mettre à jour en interagissant avec des copies d'étoiles voisines mais aussi des copies d'étoiles de la constellation de référence.
En termes de programmation logique, la constellation de référence est la base de connaissance et l'espace d'interaction est un ensemble de requêtes. Contrairement à la programmation logique (par exemple en Prolog), il n'y a aucune vraie distinction entre une requête et une autre clause. Nous avons donc un espace de résolution de contraintes avec une partie statique dont on tire des étoiles et l'autre dynamique où l'ont construit des solutions.
La constellation à gauche de `|-` est la *constellation de référence* et la constellation de droite est *l'espace d'interaction*. L'idée de l'**exécution** est que l'espace d'interaction est une zone de travail où se trouve les étoiles initiales au départ. Ces étoiles initiales vont interagir par fusion avec des copies d'étoiles de la constellation de référence mais aussi de l'espace d'interaction.
- Pour travailler avec des automates, la constellation de référence est l'automate et l'espace d'interaction démarre avec l'encodage d'un mot.
- Avec des programmes logiques, on aura la base de connaissance d'un côté et la requête de l'autre.
- Avec les preuves de la logique linéaire, on aura la structure de preuve auquel on aura retiré une étoile contenant un atome libre pour la placer dans l'espace d'interaction. Les structures de preuves, contrairement aux automates et programmes logiques, peuvent être exécutés par n'importe quel point d'entrée. Plusieurs choix sont donc possibles.
