SMEme: A Practical Neurosymbolic AI System for User-Attributable Decision Analysis

1. Introduction to SMEme

Space Coast, FL — SMEme is a neurosymbolic architecture for user-attributable decision analysis. Directly in a chat session, a user supplies the model with the target knowledge-domain context such as policies, white papers, saved prompts, web research, and anything else their LLM harness can consume. With guidance from SMEme MCP tools, the model is instructed to generate a decision tree consisting of natural-language questions with answer options, branching conditions, and possible conclusions. Without leaving chat, the subject-matter expert reviews, edits, and authorizes that tree in ordinary domain language, as text or through multi-turn chat with their agent. The authored tree is persisted as a versioned decision tree graph (DTGraph), and the agent can ask SMEme to validate its graph structure. Once saved, the tree appears on the user's SMEme dashboard. From there the user has authority to create, download, and delete it and can edit the tree manually as JSON, through SMEme's graphical editor, or with their agent's help in chat.

Only when a user clicks "Deploy" from the SMEme dashboard or editor is the DTGraph deterministically compiled into a frozen intermediate representation (IR). Redeploy after edits to the DTGraph is a new commitment and generates a new IR; prior IR stay in the database for audit of solver results made under them. The expert-authorized object remains the decision tree (DTGraph); the IR is the deterministically compiled machine-facing encoding of that authorized structure, tightly coupled to it. If the user ever deletes a decision tree, the DTGraph and associated IR are deleted with it. This is the first user-attribution gate for the logical structure of permissible automated reasoning that can happen downstream. This also enhances user agency by providing them the opportunity to fully review and consent to the correctness of the decision tree versus opaque LLM "reasoning tokens" or an inaccessible knowledge-engineer translation of the domain knowledge.

When the user is ready to run a set of facts and/or assumptions against the decision tree, the solver loads the current persisted IR and, with fixed program code—an implementation of SMEme's Decision-DAG Calculus (Arista Labs, 2026)—encodes it into the propositional theory T(IR). That theory is not stored; it is compiled on demand and added to a symbolic constraint solver instance at each request to ensure what the solver reasons over is deterministically compiled from what the user approved by that request.

flowchart LR
    DT["User-approved decision tree
(DTGraph)"]
    IR["Intermediate representation
(immutable IR)"]
    T["Propositional theory
T(IR)"]

    DT -->|"Deploy: compile and persist"| IR
    IR -->|"Evaluate: encode on demand"| T

SMEme provides two evaluation modes over the same deployed theory. In Inquire, SMEme's backend symbolic constraint solver selects the next reachable unanswered question identifier that can still change the outcome. The orchestration layer uses that identifier to retrieve one blind task. That task carries a question identifier, question text, and allowed answer options drawn from the frozen worksheet catalog. Critically, the overall graph topology is withheld from the task payload so the LLM cannot see other questions, branching conditions, or possible conclusions. That withholding, along with MCP tool guidance not to use cached context or memory to infer those facts, attempts to ensure the LLM cannot be influenced by that context when tasked with answering that single question.

The user can provide their agent any context the LLM can process to draw answers from, such as local files, charts, pasted data, and whatever the agent can access via other MCP tools like CRM, email, and web drives, and so forth. The user can also ask the agent to present the next question and answer choices for them to answer themselves. Deterministic evidence collection workflows can be run given that the questions and their answer choices for any given decision tree are known in advance. In any case, while in Inquire mode, an answer must be accompanied by a provenance_id. That identifier is opaque to SMEme's logical layer. The surrounding agent or harness can associate it with a human-inspectable source, so the user can check the proposed answer against that source. Provenance records where the proposed answer came from. It does not certify that the source supports the answer.

The agent submits the answer via SMEme MCP tools. It passes through a structural validation gate and is then admitted as evidence E. The provenance_id is retained separately as provenance where the evaluation path supports it. Any explicit operational assumptions A are also added to the solver. These are optional reachability constraints rather than answers. The caller may force named nodes reachable or unreachable (force_reachable_ids / force_unreachable_ids) without adding option literals to E. Overlapping force-reachable and force-unreachable ids are rejected before the solver.

Apply shares theory and evidence projection with Inquire but not the same stopping rule. It can report a unique result where Inquire would still ask another question. The caller instead submits a structured worksheet of each question in the tree and any answers that they include. SMEme validates and evaluates them in a single batch call to the solver. A structured citation (excerpt, locator) is optional in this mode. Apply is useful for batch processing, integrations, regression tests, and audits in which evidence has already been collected or the complete submitted answer set needs to remain visible.

In either mode, a solver computes logical consequences over constraints T(IR) ∧ E ∧ A, leaving unanswered questions open rather than treating them as false. E is admitted option literals and A is kept out of E so that adding answers remains conjunctive extension (§2). If admitted assumptions make the working base unsatisfiable, the case is assumptions_inconsistent, not a conclusion. The expert never reads or writes a formula or ontology expression, and requires no specialized formal-logic training. The model does not interpret the constraints or branching logic or compute their formal consequences. Only the symbolic constraint solver computes the logical consequences of the user-approved decision tree, admitted evidence, and any assumptions.

flowchart TD
    C["Domain context"] --> P["Model proposal"]
    P --> D["Expert-reviewed decision tree
(DTGraph)"]
    D -->|"Deploy"| I["Validated IR
(immutable compiled artifact)"]

    S["Case sources"] --> EP["Agent evidence proposal"]
    EP --> G["Structural admission gate"]
    G --> E["Admitted evidence (E)"]
    A["Assumptions (A)"] --> B["Working base
T(IR) ∧ E ∧ A"]

    I -->|"Encode on demand"| B
    E --> B

    B --> Q["Next blind question"]
    B --> R["Structured report"]
    B --> X["Counterfactual and support diagnostics"]

This suits decision support and logical analysis in domains whose rules can be expressed as explicit criteria and branches. Some applicable domains include regulatory and policy compliance, medical and legal decision support, diagnostics, troubleshooting, underwriting, eligibility, and, critically, AI governance.

Revision: Live, Stale, and Redeploy

When the author changes the tree, those edits do not become the theory until they click Redeploy in the web editor. Each evaluation is stamped with the artifact it used, so a result stays interpretable under the rules it was evaluated against. The dashboard marks the tree Live when the saved graph matches the deployed snapshot and Stale when it does not. Evaluate refuses a stale graph with stale_theory. A review date on the tree appears as review_overdue on agent and MCP responses. Deploy and Redeploy are not MCP actions, and a wrong extraction in one case does not generate a proposed revision of the tree.

2. The reasoning regime

The propositional logic underlying SMEme's backend reasoner is sound, complete, and decidable over a finite atom space. The expert reviews the tree rather than a formula, and the semantic machinery stays limited to Boolean valuations and classical connectives. Z3 supplies a mature SAT decision procedure for that core (de Moura & Bjørner 2008). Entailment reduces to satisfiability. T(IR) ∧ E ∧ A ⊨ p iff T(IR) ∧ E ∧ A ∧ ¬p is unsatisfiable.

T(IR) is the conjunction of three kinds of constraint. Guard interpretations tie each edge guard, the condition on an edge from one node to the next, to an option atom or to true. Reachability-scoped exclusivity, reach(q) → ExactlyOne(options(q)), forces one option only where the question is reached. A reachability recurrence equates each non-entry node's reachability with the disjunction of its guarded incoming paths, and the entry node is asserted reachable. Material implication is therefore scoped by reachability. When reach(q) is false, the implication is vacuously true and the question's options are left unconstrained. Those option values cannot activate a downstream node because every reachability term requires both a reachable source and an active guard. Separately, SMEme checks consistency before reporting consequences, so an unsatisfiable working base is returned as inconsistent rather than allowing classical explosion to appear as arbitrary entailments.

SMEme trusts graph validation, graph-to-IR normalization, compilation, solver encoding, Z3, and result interpretation. The engineering value is that this trusted path is modular and built around a small semantic core that can be specified and tested independently. Finite atom spaces make the regime decidable, while practical performance at deployed sizes depends on instance size and structure—principally reachability constraints plus guarded exactly-one groups—even though satisfiability remains NP-complete in the worst case.

Why not a more expressive commitment language

Modal or first-order targets and non-standard semantics/inference rules turn expressiveness and authorizability in opposite directions. A more expressive logic admits a larger space of faithful-looking mistranslations and narrows the population of users competent to catch them. Increasing expressiveness can sacrifice decidability, increase worst-case complexity, enlarge the trusted translation surface, or make expert review harder. Encoding those relations through additional questions can duplicate state and expand the atom and path spaces. Relations that cannot be reduced upstream to truth values over a finite set of authorized propositions cannot be represented in SMEme's symbolic layer. SMEme deliberately pushes requirements outside its propositional fragment into upstream deterministic procedures rather than expanding the solver language.

Closed language, open completions

This is the most important semantic commitment in the system and the one most often misread. Unanswered is absence of evidence, resolved by asking. A "don't know" answer option to a question is admitted evidence about absence — a fact the constraints can branch on (e.g. "if submitted answer is 'don't know', go to question 9"). Both are useful and conflating them would reintroduce closed-world negation through the evidence path. The language is closed. The atom space is finite and runtime input cannot invent a proposition. The world is not. Missing facts are not treated as false. Under the closed-world assumption, every option of an unanswered reachable question would be logically false, colliding with ExactlyOne (see above) and rendering the case inconsistent. Under negation as failure, failure to prove an option would assert its negation, with the same collapse. The calculus rejects both readings. Unproven is undetermined, not false.

Why adding an answer preserves earlier results and changing one does not

Adding unanswered-slot literals is conjunctive extension. If newly admitted literals Δ are added to the working base B and B ∧ Δ remains satisfiable, every remaining model is still a model of B; slots may close, but no previously possible completion is restored. If Δ contradicts B, the model class is empty and the case is inconsistent, not a stronger entailment. Changing a filled answer is not extension. It retracts the old option literals and installs another E, so the new working base is not B plus more evidence; SAT witnesses and consistency results from B do not transfer.

Named in standard terms, the consequence relation is monotonic, and answering an open question only grows the premise set, so earlier consequences persist. Editing an answer shrinks that set before it grows again, and monotonicity says nothing about a step like that.

Consequences are computed over completions:

inconsistent is a metalevel case status, not a third truth value; the object logic remains classically bivalent.

These are Decision-DAG Calculus (Arista Labs, 2026) terms, not one wire vocabulary. Kernel queries use entailed / not_entailed / possible / impossible / inconsistent. Bulk Apply reports SAT_UNIQUE, SAT_AMBIGUOUS, UNDER_DETERMINED, or UNSAT, mapped in the product report to concluded, multiple_outcomes_possible, needs_more_information, or an inconsistency kind. The layers are related but not interchangeable.

Resolved(B) versus SAT_UNIQUE

The two modes stop on different conditions. Inquire treats the case as resolved only when the working base (B) is consistent and exactly one conclusion (c) is both possible and entailed. That is Resolved(B). Entailment of c is not enough, as a subset of the evidence may force reach(c) while another conclusion remains possible.

Apply reports SAT_UNIQUE when it finds a model with exactly one true conclusion c and then cannot find a model in which c is false. That does not mean no other conclusion is still possible. Another conclusion c' can remain reachable in some models that still make c true. Resolved(B) requires the possible set and the entailed set to be the same singleton. Core has a case where Apply returns SAT_UNIQUE while Inquire still asks another question.

That case is well-formed. Deploy does not require a functional tree, a graph in which every complete assignment yields exactly one conclusion. Radio exclusivity only forces one option on a reached question. One option may activate two successors, so two conclusions can hold in the same case. Deploy fails if the theory is unsatisfiable or a declared conclusion can never be reached. Concurrent outcomes are left to the expert.

3. Diagnostics and analysis queries

Inquire and Apply ask the solver two things about the working base T(IR) ∧ E ∧ A. First, whether it is satisfiable at all. Second, if it is, whether a conclusion holds in every remaining completion, fails in every one, or still depends on unanswered slots. Consistency of the admitted answers is the first SAT check and the rest are consequence queries over the open completion space.

A case report is not the end of the reasoning. Diagnostics reuse that same procedure on a different base by dropping some of E, swapping an option, or adding reachability assumptions. None of that is a second LLM pass, and none of it is a derivation the user can replay by hand. Each result is another SAT or entailment answer, stamped to the compiled artifact it ran against. The queries that ship differ only in which base they build and what they ask of it.

Evidence sufficiency. If a conclusion already holds in every remaining completion, an unanswered question can be shown not to bear on that consequence. That is a demonstration that those facts would not change the queried result. The analysis ranges over unanswered slots in the deployed tree.

Counterfactuals. smeme_reasoning_what_if evaluates two working bases. One is the current answers. The other is a caller-supplied override. It returns a report for each side and a structural delta. Each side has its own consistency result. A witness for one proves nothing about the other. The query is a comparison under one caller-supplied alternative, including any resulting status change. It does not enumerate every admissible edit.

Reachability and repair. smeme_reasoning_list_conclusions names the conclusion space of the deployed artifact. smeme_reasoning_how_to_reach asks what would have to change to make a target conclusion entailed, or merely possible under some completion. Suggested plans are independent replacement candidates. Changing a filled answer is not conjunctive extension, so each plan is checked on its own E′. Inconsistent candidates are discarded, not presented as repairs.

Path stability. smeme_reasoning_edit_affects_path asks a narrower question. It reports whether a hypothetical override would break the current forced path, without touring the full alternate world.

Support. Decisive support (smeme_reasoning_decisive_support) computes an inclusion-minimal subset S ⊆ E that still entails the conclusion under the same deployed T(IR), with assumptions held fixed. Inquire's resolving support (S_R) is a different object. It is a minimum-cardinality subset of the admitted worksheet assignments that still resolves the case in the stronger sense of Resolved(B) (§2).

These queries do not rank which commitment the conclusion is most fragile to, and they do not certify that the tree asked every question it should have. They tell the user what follows, what still depends on missing answers, and what would have to change—under the theory they authorized and the evidence they admitted. Generating a narrative summary, asking broader follow-up questions, or taking action from the report remains the user's agent's job.

4. The Real AI Unlock LLMs Deliver

Achieving the purely deterministic IR handoff from human-user-verifiable to constraint-solver-computable described above, without complicated ontologies, formal notations, or knowledge engineers, is only plausible because of the NLP breakthrough delivered by LLMs. LLMs deliver the ability to manage the semantics of natural language in context, albeit through uninspectable, learned distributed semantics. Now neurosymbolic architectures can leave much of the natural-language and domain-specific semantics in natural-language propositions, while only the truth-functional structure of the decision procedure needs to be formalized. This NLP capability is the real unlock LLMs deliver to the longstanding AI project.

The semantic risks from standard neurosymbolic formalisms do not disappear. The model can propose the wrong decision tree or fail to correctly associate evidence with an answer, or, more colloquially, hallucinate. The mitigation has always been to treat LLM output as proposals that require the user, through reasonably diligent review, to determine that the artifacts they can inspect are free of errors and omissions before authorizing them. Put more technically, in SMEme, commitment itself has two boundaries: rule commitment is the expert's Deploy of a reviewed decision tree into an immutable IR, from which T(IR) is derived, and case commitment is the admission of evidence E and assumptions A for a particular matter. The solver is the semantic authority over T(IR) ∧ E ∧ A. Neither the user nor the LLM can modify T(IR) during evaluation; the user supplies E and A and can replace the operative rules (IR) only by revising and Redeploying the tree. Attribution and agency stay with the human user, where they belong.

Agentic tool use is another direct consequence of the LLM breakthrough in NLP. Because the model can interpret the selected question, its context, and natural-language descriptions or schemas of available tools, it can autonomously choose a procedure, construct API calls, and generate ad hoc code or structured queries such as SQL and SPARQL. The invoked tools can perform deterministic operations such as sorting, counting, calculation, parsing, arithmetic, or other formal interpretation of context. Their outputs help the model form a proposed answer; only that answer enters SMEme in the authorized vocabulary, without importing the tools' semantics into T(IR) or giving the host authority over formal consequence. That autonomy carries no formal guarantee, but the proposal and the source the agent cites are inspectable before being admitted to the solver.

SMEme is also compatible with fully deterministic evidence-gathering workflows. Because a deployed tree fixes its question identifiers and allowed answer sets, an external workflow can bind each question to a predetermined API call, database query, parser, calculation, or similar procedure and return a reproducible answer. Furthermore, the tree can easily be downloaded and shared as JSON data for peer review, testing, and colleague re-use. In any case, the resulting answer still passes through SMEme's evidence-admission gate.

5. What SMEme does not certify

The trusted path described in §2 covers compilation and consequence, not meaning. Stated plainly and in one place, SMEme does not certify:

• Tree fidelity. That the authorized tree asks the questions the governing rule actually turns on. A plausible substitute question yields exact reasoning and an unsound decision, and only expert review of the tree catches it.
• Evidence truth. That an admitted answer is correct, or that the source behind its provenance_id supports it. Provenance identifies a source; it does not vouch for what the source says.
• Artifact selection. That the model chose the right tool, constructed the call correctly, or searched the available context completely.
• Question coverage. That the tree asked every question it should have. A missing branch has nothing to perturb, so no diagnostic ranges over it.

Chat also fails closed when isolated re-extraction would be required. Ordinary conversation context may retain prior turns, so the default chat surface does not pretend that verification occurred.

Two further limits are about scope rather than certification. The architecture reaches a domain only if its expertise decomposes into explicit criteria whose dependencies and alternatives can be represented as a finite decision DAG; where judgment is holistic prior to any protocol, there is no tree to author, and a tree authored anyway would be a distortion. And these claims hold over an atom space small enough that review can be exhaustive rather than sampled. Where that threshold falls is a measurement question; no scale figures are claimed.

What SMEme does hold is narrower and mechanical. Given the deployed IR and the admitted E and A, the reported consequences are the consequences of T(IR) ∧ E ∧ A, computed by fixed, publicly available program code and stamped to the artifact that produced them.

6. How To Learn More & Cite

Every implementation claim in this document describes SMEme Core v0.9.12, commit 92a2c9365c221a1edb7645f4d2d91eea9a4b68c1, consumed by the Cloud overlay as image digest sha256:a3e14ffa25e21641f79728b1ebed6f57f3f3726f362f2f6ff000b03feaf28e0b. The public theory baseline is tag decision-dag-calculus-v1.1; the release bundles specification version 1.2. Claims resolve against that tagged release rather than against main. A description whose reader cannot identify the build being described is not checkable.

Focused unit and contract tests in that release cover graph validation, compilation, consequence queries, ingest-gate reject codes, and unanswered-as-absent behaviour. A focused audit of 81 such tests against v0.9.12 passed.

The theory baseline tagged decision-dag-calculus-v1.1 does not specify Inquire at all. Specification 1.2, bundled in this release, adds it as Part II target material in §13.9, which states that no public endpoint, MCP contract, or conformance row ships. This document describes the guided gather loop that does ship, which shares the blind task and the Resolved(B) stopping rule but not the isolated re-extraction that §13.9 requires.

Guided Inquire ships on MCP as smeme_reasoning_evaluate and smeme_reasoning_evaluate_continue. Inquire and Apply request and report shapes ship with the MCP tools named above. SMEme Core is source-available at AristaLabs/smeme. The hosted product is smeme.ai. Arista Labs is at aristalabs.ai. Questions, MCP how-to, and examples belong in GitHub Discussions.

Cite this document as Arista Labs. (2026). SMEme: A Practical Neurosymbolic AI System for User-Attributable Decision Analysis (September 2, 2026). https://aristalabs.ai/smeme-architecture.html.

References

• Arista Labs. (2026). The SMEme Decision-DAG Calculus: Finite Decision DAGs as Propositional Reachability Theories (Version 1.2; theory baseline decision-dag-calculus-v1.1). Public specification.
• de Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS 4963, 337–340.