Moteur de règles de clause Horn
Chaînage en avant sur les faits de style Prolog et les règles Horn ; interroger les objectifs et inspecter les traces de dérivation.
À propos de cet outil
Saisissez des faits et des règles de Horn positives, puis prouvez un objectif ou déduisez toutes les conséquences. Un fait ou une règle par ligne ; le point final est facultatif. Les lignes vides ou commençant par # sont ignorées.
Exemple : parent(bob,ann). Les variables commencent par une majuscule ou un trait de soulignement : ancestor(X,Z) :- parent(X,Y), ancestor(Y,Z). Chaque _ est indépendant. Les noms sont sensibles à la casse ; constantes et prédicats commencent par une minuscule. Fonctions, constantes numériques ou entre guillemets, arithmétique et négation ne sont pas prises en charge. Les faits sont sans variables ; chaque variable de tête doit figurer dans le corps.
Les objectifs peuvent contenir des variables : ancestor(dora,X) affiche les faits correspondants. Non prouvé signifie que la base ne permet pas de déduire une réponse, sans affirmer que l’objectif est faux dans la réalité. La trace montre la première déduction de chaque nouveau fait, ses prémisses concrètes et son tour. Les faits déjà connus ne créent pas de nouvelle ligne. Ouvrez les faits connus pour consulter la totalité.
Démonstrateur Datalog dans le navigateur : 12 000 caractères par champ, 300 lignes de faits, 100 règles, 8 arguments par atome et 12 prémisses par règle. Arrêt après 200 tours, 1 000 faits connus ou 50 000 comparaisons de candidats. Les déductions partielles restent valides ; les réponses manquantes restent indéterminées.
Seules les valeurs saisies sont conservées dans ce navigateur. Les résultats calculés et historiques ne sont pas enregistrés.