Faculty · AI is techLogic, notation and language-model reasoning
On this page
OverviewOldest testNotationsEngineeringExperimentsEvidenceWhere it points
DSTI TechBlog / AI is tech
Faculty AI is tech

Teaching machines to read logic

A modern language model can translate a menu and hold a fluent conversation, yet hesitate over whether a short argument is actually valid. Academic Director Hanna Abi Akl has spent much of his PhD in that gap — between an argument that sounds right and one that is right — and built a small, open Python package, Common Logic Grammar Construction (CLGC), to make the question measurable. This is the science, the engineering behind it, and an honest account of what the work achieved and what still needs improving.

syllogistic-reasoningfirst-order-logicknowledge-representationneuro-symbolic-aisemantic-websmall-language-modelsopen-science

A modern language model can draft an essay, translate a menu, and hold a fluent conversation. Ask it whether a short three-line argument is valid, and something more delicate happens. That delicate space — between an argument that sounds right and one that is right — is where I have spent much of my PhD, and it is the subject of this article.

The piece has two intertwined threads. The first is a scientific question: how do language models handle logic, and what happens when we hand a model the same logical problem written in a different formal language? The second is an engineering answer: a small, open Python package I built, called Common Logic Grammar Construction (CLGC), that makes the question measurable and reproducible. I care about both threads equally, and both connect to things we teach at DSTI: the discipline of documentation and clean code in the Warm-Up's Clean IT module and our Software Engineering (SE1/SE2) guidelines; the grammar-of-a-formal-language reflex that the relational-model and SQL (Structured Query Language) courses build — where we teach SQL as notation over relational algebra, and read a query plan as the operator tree an optimiser rewrites; the measure-one-thing-at-a-time loop of the Python Machine Learning Labs; and the model-training foundations of the Artificial Neural Networks and Deep Learning courses, which I taught and substantially reworked before handing them to their current professors. I will point at those connections as they arise, because a school blog earns its keep by showing where research meets the classroom.

This is a long read, and it is meant to be — this is the DSTI TechBlog, after all. We start from what a syllogism is, move through first-order logic and the idea of a notation, open up the architecture of the package, walk through the experiments, and — the part I value most — set out honestly what the work achieved and what remains to improve.

01 The oldest reasoning test we have

Logic, inference, and the syllogism

Logic, at its root, is about good reasoning: the ability to derive new true statements from ones we already hold. The unit is the proposition — a sentence that is either true or false. A syllogism chains two or more propositions (the premises) into a new one (the conclusion). The schoolbook example is the one everyone meets first:

All men are mortal. Socrates is a man. Therefore, Socrates is mortal.

Aristotle used arguments of this shape to open the study of logic for a good reason: the validity of a syllogism depends only on its form, not on the particular words. Replace the terms and a valid shape stays valid. Since Aristotle, logic has branched into propositional logic, first-order logic, and the mathematical logic of Frege and his successors — many ways to write down the same underlying forms.

When the words pull one way and the form the other

Consider a second argument:

All cars are vehicles. No animal is a car. Therefore, no animal is a vehicle.

The conclusion feels sensible — animals are not vehicles — yet the argument is invalid: the premises forbid animals from being cars, and say nothing that forbids an animal from being a vehicle. Everyday plausibility points toward "valid" while the form says "invalid". That gap has a name: the content effect (a close relative of belief bias) — judging an argument by how believable its conclusion sounds rather than by its structure. People show it, and models trained to predict likely text show it too, since plausibility is exactly the kind of signal that training rewards.

This is what makes syllogisms such a clean instrument. They are small; their validity is decidable by form; and they let us measure the degree to which a reasoner leans on content versus structure. So the modern question becomes sharp and testable: when a model labels a syllogism correctly, is it reasoning about the form, or leaning on the familiarity of the words? The two-part series Logic in the Era of Artificial Intelligence sets up exactly this (Part 1) and answers it with a tool (Part 2).

02 The same thought, written many ways

First-order logic: writing the form down

To study form, we first write it down. The standard tool is first-order logic (FOL): quantifiers (∀ "for all", ∃ "there exists"), connectives (→, ∧, ∨, ⊕ "exclusive or", ¬), variables and predicates. The Socrates argument becomes:

∀x (Human(x) → Mortal(x))
Human(socrates)
∴ Mortal(socrates)

The translation removes tone and connotation and keeps the skeleton. Anyone who has turned a vague business request into a precise SELECT … WHERE … has performed the same motion: natural language in, an exact formal expression out. SQL is itself a formal language with a grammar — and beneath its surface sits relational algebra, a closed set of operators over sets of rows (σ select, Π project, ⋈ join …). Written one operator per step, a query is a tree: the same logical plan a database builds from your SQL. That tree can then be rewritten into provably-equivalent ones — push a selection below a join to filter early, reorder joins because ⋈ is commutative and associative — so long as you never project away a column a later step still needs. Sébastien and I teach the algebra first, on purpose, so students read SQL as notation over that form and a query plan as an operator tree: the algebra fixes what is correct and which rewrites stay legal, while the query optimiser, costing plans against table statistics, decides how fast. It is the same grammar → tree → transform motion this article keeps returning to — the optimiser is just another pass over a syntax tree.

A spectrum of notations

FOL is one way to write the skeleton, and far from the only one. The same logical content lives in many knowledge-representation (KR) notations, and John Sowa — whose Common Logic work the name CLGC honours — spent a career arguing that these notations are the real human-machine interface. The families the project works with:

The same syllogism — the Athenian/Greek/mortal one shown in Plus-Minus above — makes the point concrete when CLGC actually generates it. The cells below are the tool's actual fol_to_* output (each statement's newline shown as a line break, surrounding whitespace trimmed), not hand-idealised:

Notation The syllogism, exactly as CLGC emits it
Natural language Every Athenian is a Greek. Every Greek is mortal. Therefore, every Athenian is mortal.
FOL (source) ∀x (Athenian(x) → Greek(x))
∀x (Greek(x) → Mortal(x))
∀x (Athenian(x) → Mortal(x))
CLIF forall x (athenian(x) implies greek(x))
forall x (greek(x) implies mortal(x))
forall x (athenian(x) implies mortal(x))
CGIF [@every *x [(athenian[(?x)] greek[(?x)])]
@every *x [(greek[(?x)] mortal[(?x)])]
@every *x [(athenian[(?x)] mortal[(?x)])]
]
TFL -+A1-+G1-+G2-+M2-+A3-+M3
TFL+ -(+A0-+G0)-(+G0-+M0)-(+A0-+M0)
CLINGO (ASP) forall (athenian(x) -: greek(x))
forall (greek(x) -: mortal(x))
forall (athenian(x) -: mortal(x))
MINIFOL all:x (athenian(x) :- greek(x))
all:x (greek(x) :- mortal(x))
all:x (athenian(x) :- mortal(x))

The content is identical in every row; only the notation changes — and so does its shape. CLIF, CLINGO and MINIFOL keep one statement per line; TFL, TFL+ and CGIF fuse the whole argument into a single expression, and CLGC lower-cases predicate names as it translates. Prolog is not a generation target: the package validates statements against a Prolog grammar and hands them to a Prolog engine (Pytholog) rather than emitting Prolog.

A melody is the same tune on a piano, a synthesiser, or a marimba; the instrument changes what a listener notices. The scientific hypothesis of the whole project is the linguistic analogue: hand a model the same syllogism in a different notation, and its reasoning behaviour shifts — sometimes upward, sometimes not, and always in a way worth measuring. There is a strong prior for this from my 2025 study, which found that a small model could keep strong reasoning performance when natural language was swapped for a more compact logical language (hal-05248053). CLGC is the tool that turned that observation into something systematic.

03 CLGC as engineering

The science only means something if the instrument is sound, so I want to spend real time on the build. This is the part that leans hardest on the software-engineering habits we teach.

One good abstraction: a notation is an object

The core design decision is small, and I think it is the right kind of small. A notation is an object. There is one abstract base class, Notation; every formal language — FOL, CLIF, CGIF, TFL+, CLINGO, PROLOG, MINIFOL — is a child class, and each is defined by its Backus–Naur Form (BNF) grammar, the standard way to write down how valid expressions of a language are built. FOL is the first concrete class, since it is widely used and human-readable, and every other notation extends from there.

Two consequences follow, both deliberate:

  1. Adding a notation means writing a grammar, not editing the engine. A contributor supplies a new notation's BNF and CLGC can then generate and translate syllogisms in it. This is the open/closed principle in practice — open to extension, closed to modification — the sort of thing SE1/SE2 is really about.
  2. Syllogisms are objects too. A FOLSyllogism holds premises and a conclusion, and knows how to categorise, translate and validate itself. To the best of our knowledge, CLGC is the first package to treat syllogisms as first-class objects rather than as plain strings.

How a translation is actually generated

The generation algorithm is the engineering heart. Starting from a syllogism in FOL (which has a defined BNF grammar), CLGC:

  1. parses the FOL statement against the FOL grammar to build an Abstract Syntax Tree (AST) — the same tree-shaped intermediate a compiler builds from source code;
  2. constructs an equivalent tree in the target notation using that notation's BNF grammar;
  3. reconstructs the statement in the target notation from the tree, applying the target's syntactic rules (spacing, parentheses, operator symbols).
Figure — grammar → tree → emit
CLGC · TRANSLATION PIPELINE Every translation routes through an explicit grammar and tree. FOL BNF target BNF target syntax parse map emit FOL source ∀x (Human(x) → Mortal(x)) AST (source tree) ∀x Human(x) Mortal(x) target tree forall implies human(x) mortal(x) CLIF output forall x (human(x) implies mortal(x)) generate → verify the emitted string is parsed back against the target grammar (BNF); only a valid tree ships ✓
The grammar → tree → emit pipeline: FOL is parsed to an AST, mapped to the target notation’s tree, emitted as text, then validated back against the target grammar before it ships.

Because everything routes through an explicit grammar and an explicit tree, a translation is reconstructable and checkable rather than a black-box string edit. Anyone who has written a parser, or thought carefully about how SQL is parsed, will recognise the shape immediately.

See also — a house pattern. This grammar → tree → emit, paired with generate-then-verify, is not unique to CLGC; I recognise it in how Sébastien engineered DSTI's new web system from June 2026. That build ships one pruned stylesheet per page by parsing CSS (Cascading Style Sheets) into a recursive tree and re-checking each pruned page against the original before it ships; its schema.org checker is constructed from schema.org's own vocabulary rather than hand-coded rule by rule; and its governed translation pipeline treats a translation as a structure-preserving transform confirmed by a deterministic validator. Different problems, one way of thinking — define the target formally, work on the tree, and prove the output before it goes out. That consistency across the school's engineering — told in full across the two-part engineering TechBlog, Part 1 and Part 2 — more than any single tool, is the thing I find worth pointing at.

The four questions to ask of any new notation

When defining a new notation, the project recommends four guiding criteria — and they double as a neat lens on the whole research question:

The MINIFOLx family exists precisely to probe the Frequency criterion. Each variant makes a small, deliberate change to FOL: MINIFOL swaps the operator symbols (∀, ⊕, →, ¬, ∃, ∧, ∨) for the strings all, ^, :-, -, some, &, |; MINIFOL2 drops the existential quantifier; MINIFOL3 writes not for ¬; MINIFOL4 writes , for ∧. These are lightweight, and by design unfamiliar — a way to ask what happens when a model meets a syntax it has almost never seen.

What the package does, in four verbs

A short, real example from the repository:

from clgc.__base import *

syllogism = FOLSyllogism(
    "∀x (Bikes(x) → ¬Calledcars(x))\n"
    " ∀x (Bike(x) → Vehicle(x))\n"
    " ∃x (Vehicles(x) ∧ Bikes(x))\n"
)

print(syllogism.categorize())               # -> categorical
tfl_plus = FOLSyllogism.fol_to_tfl_plus(syllogism.syllogism)
print(tfl_plus)                             # -> -(+B0--+C0)-(+B0-+V0)+(+V1++B1)

That last line is the same thought wearing a very different coat.

Playing well with others

Because CLGC validates against grammars, it cooperates with existing logic tooling instead of reinventing it. The repository shows CLGC handing validated statements to Pytholog, a Prolog engine for Python: each candidate fact is validated as PROLOG by CLGC before it is added to a knowledge base and queried. Validation-before-insertion is the logic-programming version of checking inputs at the boundary — the same instinct that keeps a data pipeline honest.

The Clean IT dimension

CLGC installs with pip install clgc, carries a README that documents its architecture and every supported notation, and is archived with a citable record on HAL and Software Heritage. None of that is glamorous; all of it is the difference between a script that runs on one laptop and a tool other people can build on. The Clean IT module in the Warm-Up exists to make that second thing ordinary, and a package other researchers can install and cite is the visible proof that the habit took.

04 The experiments, in full and in the open

With the instrument built, the science becomes tractable. The central question: does the choice of notation change how well a model reasons about syllogisms — and can the right framing help a small model attend more to structure and less to content?

The task, the data, the models

The studies build on two public, human-curated reasoning datasets, FOLIO and P-FOLIO, which already give syllogisms in natural language (NL) and FOL. CLGC extends each across the supported notations to produce FOLIO-KR and P-FOLIO-KR, both released openly on Hugging Face. The task is a three-way classification: label each conclusion True (valid), False (invalid), or Unknown (inconclusive). The datasets are honestly uneven — in the truth labels, and in the SEF categories too (in FOLIO-KR the categorical category is far outnumbered by disjunctive and complex) — so the papers report the F1 score rather than raw accuracy where the truth-label imbalance matters.

The SEF side of the pipeline sorts every syllogism into one of four structural categories, each with a precise definition the model can be shown:

Those four categories are the SEF as the papers define it conceptually. The shipped categorize() method is a lightweight keyword-and-shape heuristic that approximates that scheme rather than computing it exactly: it labels a syllogism disjunctive when the text contains a disjunction symbol (∨ or ⊕); otherwise complex when it runs to more than three statements; otherwise categorical when the lower-cased text contains one of a small set of quantifier words (all, any, some, no, few, most, none, several) as a substring; and hypothetical as the default fall-through. It is fast and good enough to bucket a dataset at scale, but it is a heuristic that stands in for the formal definitions above, not a re-implementation of them — worth keeping in mind when reading category-level results.

Two model regimes are compared. In Supervised Fine-Tuning (SFT) the model trains on syllogisms in a given notation with their labels, then predicts on held-out ones; the workhorses are the small, encoder-decoder Flan-T5 models (small and large), chosen for frugality and reproducibility. In Zero-Shot (ZS) the model is asked cold, with two prompt scenarios: Scenario 1 gives the syllogism plus the notation's BNF grammar; Scenario 2 adds the SEF category, its definition and a worked example, to see whether telling the model what kind of argument it is looking at helps. The ZS models are small decoder-based systems under ten billion parameters — Gemma-2-2b-it, Llama-3.2-3b-instruct, Phi-3.5-mini-instruct. The Python ML Labs run on exactly this shape of work: fix a metric, change one thing, read the result honestly.

What the results show

Several findings come through across the studies, and I will state them as they are.

Model size lifts performance, largely independent of the notation. As Flan-T5 scales from small to large, most notations improve together. That gives a clean baseline: scale helps everywhere, so the interesting effects are the ones that remain once scale is accounted for.

Which notation wins depends on the model and the dataset. On P-FOLIO-KR with the small model and very little training data, the compact, abstract TFL+ did unexpectedly well — its +/- tokens are already familiar to the tokeniser, so a short notation gave the small model something firm to stand on. With the larger model, NL regained the lead. Reading that honestly means resisting a single tidy headline: the effect is real, and it is conditional.

A hybrid framing makes reasoning more careful. Pairing NL with a compact formal notation shifted models toward more conservative judgements. In the RuleML+RR study, NL + CLIF in particular improved reasoning by refutation — spotting the invalid cases — and was consistently the strongest at the hardest label, Unknown; in the SemEval study, NL + FOL lowered the content effect relative to NL alone. For systems that otherwise tend to answer confidently when they should hold back, a framing that nudges toward "Unknown" when warranted is a genuinely useful property.

Compact notations run faster. In the ZS timing, NL was the most computationally expensive notation to process, while compact notations such as TFL+ and CLIF ran quicker; CLIF sat at a sweet spot between speed and quality. Where a notation keeps accuracy while shortening the input, it buys inference speed for free — welcome news for anyone running models on a budget.

Category descriptions help, conditionally. Adding the SEF category to a ZS prompt (Scenario 2) raised performance for several model/notation pairs and left others flat. The gain depends on how sensitive a given model is to the notation, which is itself an interesting result about how these models use extra structure.

The SemEval companion put numbers on the bias. In the SemEval (Semantic Evaluation) 2026 Task 11 study (Subtask 1: Disentangling Content and Formal Reasoning), the strongest small model — a Flan-T5-large pre-fine-tuned on FOLIO and then fine-tuned on the task, reading NL + FOL — reached 90.57% accuracy with a Content Score (CS) of 27.80% on the blind evaluation set, ranking 10th on accuracy and 7th on the content-effect metric. The Content Score deliberately rewards accuracy while penalising the content effect — CS = ACC / (1 + log(1 + CE)), where ACC is accuracy and CE the content effect — so a strong score is hard to earn, and earning a competitive one with a sub-billion-parameter model, while lowering the content effect relative to NL alone, is the part I am glad about. The natural-language-to-FOL step in that pipeline used a commercial model, with translations checked by hand on a 20% sample of the training set and on the entire evaluation set.

What remains to improve

An honest experiment reports the parts that resisted, and these point straight at the next work.

Catching invalid arguments is the harder skill. The models recognised valid syllogisms readily and made most of their mistakes on the invalid ones, tending to accept an invalid argument as valid (a false-positive pattern). Confirming that something fits is easier than proving that it is broken; the next gains sit in strengthening refutation, and the conservative NL + CLIF framing is one promising route toward it.

The datasets are uneven. Categorical syllogisms dominate the working sets, which makes some category-level conclusions provisional. Balancing the SEF categories is a concrete next dataset task, and the papers name it as such.

One step leans on a commercial model. The natural-language-to-FOL translation currently uses a hosted commercial system. That keeps the front of the pipeline strong today, and it also creates a dependency: if the external model changes, the first link can move underneath the experiment. Naming this openly is the point — reproducibility is a property one protects on purpose.

The result I stand behind is the shape of the finding, which held across more than one study and venue: how a problem is formulated changes how a small model reasons about it, and a well-chosen hybrid framing helps it attend to structure and hold back when it should. The precise numbers live in the papers, and the open code and datasets let anyone re-run them.

05 The evidence, in the open

Common Logic Grammar Construction (CLGC) project logo
CLGC — open on GitHub and PyPI, archived and citable on HAL and Software Heritage.

Everything behind this article is public.

The work grew inside the Wimmics team (Inria, CNRS, I3S, Université Côte d'Azur), where I have been a member since early 2023, and it is the core of my PhD with Prof. Fabien Gandon and Prof. Catherine Faron, with Pierre Monnin as a close collaborator. It was supported through the France 2030 plan by the French National Research Agency (ANR), the Université Côte d'Azur Initiative of Excellence, the 3IA Côte d'Azur institute (one of France's Interdisciplinary Institutes for Artificial Intelligence), the university's high-performance computing centre, and DSTI School of Engineering. Naming the lineage matters: these ideas sit inside a larger programme on knowledge graphs, the semantic web, and neuro-symbolic AI.

06 Where this points

The direction is one I find genuinely worth pursuing. If a small, frugal model can be helped to reason about structure — by choosing how a problem is written, and by telling it what kind of problem it is — then two doors open.

The first is ontology engineering. Building the formal vocabularies and rules that let machines share meaning is careful, costly work; a model that reasons reliably over compact formal notation could take on more of the scaffolding, with a person keeping judgement over the result. That is the PhD question CLGC was built to serve.

The second is traceable reasoning. Because CLGC keeps the logical form explicit at every step — grammar, tree, translation, category, validation — the path from a natural-language question to a machine's answer stays inspectable. A reasoning system whose steps can be read is a system whose mistakes can be found, which for anything that matters is worth more than a point of accuracy. The dichotomy between natural and abstract notations points toward multi-stage, neuro-symbolic pipelines that use natural language as a first step and refine in a compact formal notation — a concrete line of future work.

There is plenty left to do: balancing the datasets, strengthening the detection of invalid arguments, and reducing the pipeline's dependence on any single external model. Each is a specific next experiment, and each is easier to run because the tool underneath is clean.

If you are a DSTI student reading this, the through-line from a Warm-Up exercise in documenting your code, to a Notation base class with a tidy grammar, to a paper at a reasoning conference, is shorter and straighter than it looks in week one. I can say that with some confidence: I sat where you are, finishing my own MSc in Data Science & AI here in 2018. Build the small thing well, write down what it does, measure honestly, and share the evidence. The rest tends to follow.

Corrections and pull requests are welcome — the repository is the best place for the latter.