Idées générales

Idée : langage naturel → IR → langage formel

Syntaxe POO instancié

On code et au fur et à mesure ça rajoute nos définitions dans une STDLIB partagée

Extraits de code

// ============================================
// PRIMITIVES -- le sol du langage
// indéfinissables, fournies par le moteur
// ============================================

primitive {
    exists(Entity)              // x existe
    equals(Entity, Entity)      // x est identique à y
    before(Entity, Entity)      // x précède y dans le temps
}

// ============================================
// CORE -- première couche, non modifiable
// ============================================

// classe racine dont tout hérite
class Entity {}

// ============================================
// deuxième couche -- causalité et espace
// ============================================

class Entity {
    relation {
        causes(Entity b) {
            before(this, b)
            exists(this) -> exists(b)
        }

        affects(Entity b) {
            causes(b)
            -equals(this, b)
        }
    }
}

// ============================================
// troisième couche -- humain et action
// ============================================

class Action : Entity {
    property {
        intentional
        forced
        -intentional -> forced      // si pas intentionnel alors forcé
    }
}

class Proposition : Entity {}

class Human : Entity {
    property {
        mortal
        rational
        free -> responsible         // si libre alors responsible
    }

    relation {
        executes(Action a) {
            exists(a)
            causes(a)
        }

        intends(Action a) {
            before(this.state, a)   // l'état mental précède l'action
            causes(this.state, a)   // l'état mental cause l'action
        }

        does(Action a) {
            executes(a)
            intends(a)
        }

        asserts(Proposition p) {
            causes(exists(p))       // h contribue à l'existence de p
            -refutes(p)
        }

        refutes(Proposition p) {
            asserts(-p)             // h affirme la négation de p
            -asserts(p)
        }

        argues(Proposition p) {
            asserts(p)
            causes(exists(p))
        }

        believes(Proposition p) {
            argues(p)
            -refutes(p)
        }
    }
}

// ============================================
// quatrième couche -- philosophe
// ============================================

class Philosopher : Human {
    relation {
        theorizes(Proposition p) {
            argues(p)
            causes(exists(p))
        }
    }
}

// ============================================
// STDLIB -- extensible par l'élève
// ============================================

class Tyran : Human {
    property {
        cruel -> immoral
    }
    relation {
        oppresses(Human h) {
            causes(h.-free)         // cause la non liberté de h
            affects(h)
            -believes(h.rights)     // ne croit pas aux droits de h
        }
    }
}

class PoliticalAction : Action {
    property {
        legal
        illegal -> unjust           // si illégal alors injuste
    }
}

// ============================================
// INSTANCES
// ============================================

autonomie_morale : Proposition {}
determinisme : Proposition {}
droits_naturels : Proposition {}

socrate : Philosopher {
    believes(autonomie_morale)
    argues(autonomie_morale)
    refutes(determinisme)
}

kant : Philosopher {
    theorizes(autonomie_morale)
    theorizes(droits_naturels)
}

cesar : Tyran {
    -free
    oppresses(socrate)
    does(assassination)
}

assassination : PoliticalAction {
    intentional
    illegal
}

// ============================================
// REQUETES
// ============================================

socrate.mortal ?
// true
// chain {
//     socrate : Philosopher
//     Philosopher : Human
//     Human has property mortal
//     therefore true
// }

socrate.responsible ?
// false
// chain {
//     free -> responsible
//     socrate is -free (not declared as free)
//     therefore false
// }

cesar.responsible ?
// false
// chain {
//     free -> responsible
//     cesar is -free
//     therefore false
// }

cesar.unjust ?
// true
// chain {
//     cesar does assassination
//     assassination is illegal
//     illegal -> unjust
//     therefore true
// }

assassination.forced ?
// false
// chain {
//     assassination is intentional
//     -intentional -> forced
//     assassination is intentional
//     therefore false
// }

socrate.believes(autonomie_morale) ?
// true
// chain {
//     socrate argues(autonomie_morale)    // déclaré
//     socrate -refutes(autonomie_morale)  // non déclaré donc false
//     believes = argues + -refutes
//     therefore true
// }

cesar.believes(droits_naturels) ?
// false
// chain {
//     cesar oppresses(socrate)
//     oppresses -> -believes(h.rights)
//     droits_naturels is rights
//     therefore false
// }

• primitives — exists, equals, before — le sol indéfinissable
• : "est un" partout, héritage de classe et d'instance
• • négation
• > implication
• core non modifiable, construite en couches depuis les primitives
• stdlib extensible par l'élève
• why le moteur explique toute la chaîne d'inférence

Workflow

1. Tu écris ton argument directement

Tu ne déclares rien à l'avance, tu commences par les instances et les faits comme si tu rédigeais normalement.

2. Le moteur te stoppe sur chaque concept inconnu