I.
I only really got into LLMs recently, and until then I was completely oblivious to where all the tooling was, i.e. agents, memory tools, harnesses, etc. I ramped into it by realizing that whenever I hit a snag, I could ask Claude to explain how to get out of that snag. It worked well enough, I guess. I eventually got off the desktop app and started using Claude Code, and learned about memory-management tools to help out with the growing complexity of the things I was trying out. I setup Hindsight wrong and burned all my Opus tokens one afternoon. A few days after, I signed up for Max x20, and the next few weeks have become a haze in my memory, because I was trying everything out. Every problem I ran into, I XY questioned my way into what I thought was the solution.
I would eventually learn practically that cheap code does not translate into systems design prowess. I thought I was going to be able to keep the ball rolling and eventually get to a tool that's publishable, but I'm not quite there yet, so this is a post describing what I tried to do and some of the issues I ran into, which is very much underselling things, because some of the issues were capital P Problems. You can't Claude your way out of Problems.
One of those days in that haze, I decided I wanted a memory tool for my coding agents, rather than just relying on Claude's prose files or something else. Because I was so drunk with the power to completely obliterate NIH syndrome, I thought “hey, can't be that hard”. I wanted some database to store what agents learn and bring it back on every session, quickly, locally. An agent wrote most of it under my direction — Rust daemon, because of course it's gotta be in Rust. I guess somewhere along the way we decided facts are never deleted (only superseded, so the bank remembers what it used to believe), four retrieval strategies fused and reranked by small local models. It sounded like it worked. Claude was really confident about that part. I understood that I got it to build a search engine over a weird corpus.
After building that small proof-of-concept quickly, I wanted to build something more ambitious. LLMs are powerful, surely they can show whenever a memory contradicts another memory? I wanted it to flag contradicting memories automatically. Can't be that hard. A bank accumulates months of extracted facts, some go stale, some are wrong, and a memory that contradicts other memories without explanation is worse than no memory, because then the context window is polluted with a bunch of bullshit.
Can't be that hard.
II.
I don’t design systems for a living. What I had was an agent that found research papers whenever I asked it to find “the state of the art” in some area. I read the abstracts and whatever I could understand of them. If I thought it could help, I'd get Claude to build them, and then it implemented them while I sort-of followed along. And the loop is intoxicating: paste a paper, say “we should do that,” and by evening there’s a compiling implementation, tests, sometimes a machine-checked proof. From the inside, “sort-of following along” really feels like you're doing something productive.
So I kept hitting snags, and for each of them, I asked Claude to think harder and reach for more esoteric stuff I had probably heard somewhere. I took one semester of philosophy of language at university, and therefore I knew some basics of Logic, so naturally I figured that qualified me to "design” a contradiction checker, a “reasoning council” — abduction proposes causes, deduction certifies, induction learns candidate rules. Claude then said “hey dude, the council’s verdict model should get machine-checked to form a proper Belnap lattice, the four-valued logic where ‘not recorded’ and ‘contradicted’ are different values.” and I was like “yeah man, go for it”
I'm not entirely irresponsible. I was concerned about bullshitting this design too much so of course, I asked Claude to prove its designs. There were Agda proofs, which were later ported to Cubical Agda, a thing I definitely cannot explain to you. If it runs it's sound, right? There was a Petri net of every subsystem. There was a plan language whose replay properties were proved before its parser existed. I had a solver, a proof assistant, and the faintest idea of what was happening at this point.
III.
It’s been a few months since I started. This memory tool sort-of works. It stores memory with some decent classification. Does it actually flag contradictions? No. It doesn't yet do what I wanted to do from the start. I keep thinking about ways to word this to Claude, thinking that maybe some magic set of words will let me vibe-code my way into success. Today's try was something along the lines of, “why aren't prose memories being encoded into ASP programs automatically? how hard can it be?”
It's really fucking hard. I should have realized this by the huge pile of research papers I’ve compiled and read almost none of them. It's a worse version of buying a huge amount of books that one day I'll surely read, because at least with the books I might end up actually reading them one curious day. 86 research papers saved to Zotero about topics I barely understand are much more likely to just rot away.
Tonight, I realized I did lose the plot entirely. Claude explained in Claudese with all the load-bearing confidence that that you can't just write an ASP program for every prose memory because it turns out that's actually an unsolved problem in knowledge representation, something it called “proposition identity". After getting ChatGPT to translate what Claude had said, I then went back, “okay, explain to me what this proposition identity problem is”:
Here’s an abridged version of the answer it threw at me, with the Claudese intact:
This is worth unpacking properly, because it’s one of those problems that looks like an implementation detail and is actually a 130-year-old open question wearing an engineering costume.
The problem, stated precisely. Your conflict rules fire on syntactic equality […] So the solver never actually judges whether two memories contradict each other — that judgment was made earlier, at symbolization time, by whatever decided that two stretches of prose map to the same atom. […] Your own bank already holds the sharp form of this: fact F1 from the foundations dialogue says canonicalization “makes proposition identity syntactic” […] The rules are six lines; the identity judgment is the entire intelligence of the system.
It did explain something to me that I understood, thanks to that one semester of philosophy of language: the question of “when do two sentences express the same proposition” is really, really hard. If the checker merges fact-atoms (the smallest “currency" in this memory bank) too eagerly, it invents conflicts.
My hope was that a large enough memory bank would surface self-contradictions and that self-contradiction-surfacing would be useful enough. It doesn't need to know whether it's actually true if the current king of France is bald, but it would know some other memory said the current king of France was rocking a mohawk. Nevermind the fact there currently is no king of France (shoutout to Russell, and of course, the rabbit-abyss of denotation is a whole another can of mental whoop-ass).
And then it listed more and more papers about how hard this problem actually was. And then it explained to me that this “proposition identity” problem has been unsolved since 1892, and it told me I probably wasn't gonna crack it either. And then I decided to stop prompting Claude to write code and decided to write this post. Hopefully it was interesting to you, and if you know what I'm doing better than I am, hopefully we could chat about if any of this is salvageable. I hope it is, because it sounds like a cool project.
Claude's suggested reading list for me/us:
Philosophy — why no universal criterion exists
SEP: Propositions and Structured Propositions — the surveys of candidate identity conditions and how each fails
Frege, “On Sense and Reference” (1892) — Hesperus/Phosphorus, where it all starts
Quine, Word and Object (1960) — “no entity without identity,” the demolition
Keyword for the modern literature: hyperintensionality
KR — the engineering responses
McCarthy, “Notes on Formalizing Context“ (IJCAI 1993); Guha’s 1991 thesis on contexts
Lenat & Guha, Building Large Knowledge-Based Systems (1990) — CYC’s microtheories
Davidson, “The Logical Form of Action Sentences” (1967) and Hobbs, “Ontological Promiscuity” (1985) — reification granularity
NLP/KB — the applied problem under its searchable names
Canonicalizing Open Knowledge Bases (Galárraga et al., CIKM 2014); CESI (Vashishth et al., WWW 2018)
Universal schema (Riedel et al., NAACL 2013) — give up on identity, learn entailment
AMR (Banarescu et al., 2013) + Smatch (Cai & Knight, 2013)
Cross-document event coreference: ECB+ (Cybulska & Vossen, 2014)
Claim matching: Shaar et al., “That is a Known Lie” (ACL 2020); the CheckThat! lab tasks
LLM+ASP
s(CASP) (Arias et al., TPLP 2018); STAR (Rajasekharan et al., ICLP 2023); AutoConcierge (Zeng et al., 2023)
Distilling ASP rules from LLMs (Eiter, Higuera Ruiz & Oetsch, TPLP 2026)
NeurASP (Yang, Ishay & Lee, IJCAI 2020); ILASP (Law, Russo & Broda, JELIA 2014); FastLAS (AAAI 2020) — the rule-learning side
Practice
Wikidata Help:Qualifiers and Property proposal — the shipped, at-scale answers to context and vocabulary governance
Search strings, since the problem has no single name: "open knowledge base canonicalization", "relation canonicalization", "cross-document event coreference", "previously fact-checked claim detection", "granularity problem" propositions, "microtheories" context.
The contradiction-detection wall you hit is real, but I think it's only
load-bearing because of where you put it. Full disclosure, we build kgai,
shared decision memory for dev teams, so this is the case we care about.
For a decision, supersession is an explicit event at write time. The person
recording "we're moving off X to Y" says so, and the old fact retires with
a link. You don't detect the contradiction later, you record it when it
happens. Model-driven contradiction detection belongs at the fallback layer,
for facts that arrived sideways, not the foundation. Different problem than
the general-purpose fact bank you were building.
Hey, this seems familiar.