Goal: Transform formal proof traces into fluent, understandable natural language explanations.
Why it matters: Formal reasoning is only valuable if users can understand and trust the conclusions. Clear explanations enable verification and build confidence in AI-assisted decisions.
// Formal proof trace (machine-readable)
{
"goal": "isA Socrates Mortal",
"method": "rule_application",
"rule": "@r1 Implies (isA ?x Human) (isA ?x Mortal)",
"bindings": { "?x": "Socrates" },
"premises": [
{ "goal": "isA Socrates Human", "method": "direct_kb", "confidence": 1.0 }
],
"confidence": 1.0
}
"Socrates is mortal. This follows because Socrates is human, and the rule states that all humans are mortal."
Proof Trace
│
▼
┌───────────────────┐
│ Structure Analyzer│ ← Identify proof pattern
└───────────────────┘
│
▼
┌───────────────────┐
│ Template Selector │ ← Choose appropriate template
└───────────────────┘
│
▼
┌───────────────────┐
│ Slot Filler │ ← Fill template with entities
└───────────────────┘
│
▼
┌───────────────────┐
│ Fluency Enhancer │ ← (Optional) LLM polish
└───────────────────┘
│
▼
Natural Language Output
| Proof Pattern | Template | Example Output |
|---|---|---|
| Direct fact | "{subject} {relation} {object}. This is a known fact." | "Tom is a cat. This is a known fact." |
| Transitive chain | "{subject} {relation} {target} because {chain steps}." | "Penguins are animals because penguins are birds, and birds are animals." |
| Rule application | "{conclusion} follows because {premises}, and the rule states that {rule in NL}." | "Socrates is mortal because Socrates is human, and all humans are mortal." |
| Compound (AND) | "{conclusion} holds because both {A} and {B} are true." | "The system is ready because power is on and tests passed." |
| Negation | "{subject} is not {property} because {reason}." | "Penguins cannot fly because they are flightless birds." |
| Level | Description | Use Case |
|---|---|---|
| Minimal | Just the conclusion | Quick answers, dashboards |
| Summary | Conclusion + key reason | Reports, notifications |
| Detailed | Full proof chain in NL | Audit trails, debugging |
| Educational | Step-by-step with explanations | Learning, training |
Minimal: "Socrates is mortal."
Summary: "Socrates is mortal because all humans are mortal."
Detailed: "We can conclude that Socrates is mortal. The reasoning is as follows: First, it is established that Socrates is human (known fact from the knowledge base). Second, there is a rule stating that if something is human, then it is mortal. Applying this rule to Socrates, we derive that Socrates is mortal."
Educational: "Let's trace through how we know Socrates is mortal. We start with what we know: Socrates is human (this is given as a fact). Now, we have a rule in logic that says 'All humans are mortal' – this means if we know something is human, we can conclude it is mortal. Since Socrates is human, we apply this rule and conclude: Socrates is mortal. This is called 'modus ponens' – a fundamental logical inference."
// LLM polishing prompt
const prompt = `
Improve the fluency of this explanation while preserving ALL facts:
Original: "${templateOutput}"
Requirements:
- Do NOT add, remove, or change any facts
- Improve grammar and natural flow only
- Keep it concise
- All entities from original must appear
Improved version:
`;
Templates can be defined in multiple languages:
| Language | Template (rule application) |
|---|---|
| English | "{conclusion} follows because {premises}, and the rule states that {rule}." |
| Romanian | "{conclusion} follows because {premises}, and the rule states that {rule}." |
| French | "{conclusion} découle du fait que {premises}, et la règle stipule que {rule}." |
| German | "{conclusion} folgt daraus, dass {premises}, und die Regel besagt, dass {rule}." |