A little project similar in hopes to SEQUEL

[Juan Kat]

I found Shen while trying to solve a practical problem: I wanted an AI writing assistant that could help clarify arguments without quietly becoming the authority on what the argument means. That led me to SEQUEL, Shen, and your recent work on collaborative automated reasoning with ChatGPT and THORN.

I’ve built a small experiment in that direction, though at a much humbler level: not theorem proving, but argument linting. The AI translates prose into explicit Shen facts; Shen derives structural warnings; the AI explains only those warnings; and the human remains responsible for correcting the meaning.

I fear I've taken the project as far as I could, but if any are willing to help, here's a link: 
github-repo

[dr.mt...@gmail.com]

I need to look at this more closely.  But an initial response is that

the work is precisely in the area where Shen excels.   Shen is 

significant to the programming community as a metalanguage

for the analysis of other languages.     This would include type

checkers for other  language, and logical analysis of programs

including syntax etc.    You're actually working within that space

but you've chosen natural language as the object language.

Mark

[Juan Kat]

Thanks, Mark. I think I see the distinction more clearly now.

My reason for exposing the intermediate material was not that I think KL, or any machine-level representation, is the right thing for the user to debug. It was more about auditability: I do not yet trust an LLM to translate natural language into formal Shen structures without drift, so I wanted visible checks on what the system thinks the text means. (similar to how you found out in your chat with gpt)

But I take your point that the default frame should not be KL, or anything analogous to VM machinery. The useful object is the source-level structure: the original phrase, the claim or poetic movement being represented, the Shen-level facts/bindings derived from it, and the human-readable reason a diagnostic fired.

So perhaps the right design is a two-layer view. The ordinary view should show something like a “Shen/source frame”: source fragment, interpreted claim, bindings, rule/diagnostic, and continuation in plain terms. The lower-level representation should remain available as an audit or expert mode, not as the main debugger.

Poetry is actually one of the reasons I wanted to build this. I’m interested in whether Shen can help expose the logic of a poem without reducing the poem to paraphrase. In the example I’m attaching, the system is trying to show the translation path from poem → facts → check report → findings. I suspect your point is that this translation path is useful, but only if the visible frame remains anchored in the poem and the Shen source-level interpretation, not in generated implementation artifacts.

If that’s the right reading, then I agree: the next step is to make the audit trail more source-facing and subordinate the raw intermediate representation.

I'm attaching the files that are created as I chat with the ai. In a malformed text, findings.txt would be particularly useful. In this case, not as much. 

[dr.mt...@gmail.com]

On Saturday, 23 May 2026 at 12:55:28 UTC+1 Juan Kat wrote:

Thanks, Mark. I think I see the distinction more clearly now.

My reason for exposing the intermediate material was not that I think KL, or any machine-level representation, is the right thing for the user to debug. It was more about auditability: I do not yet trust an LLM to translate natural language into formal Shen structures without drift, so I wanted visible checks on what the system thinks the text means. (similar to how you found out in your chat with gpt)

My remarks about the unsuitability of KL for debugging were really directed at the other post (not yours).  You're

quite right not to trust LLMs.  They do make mistakes.  There is something in your work that needs to be resolved 

though which is connected to the issue you raise.

From what I understand, the LLM translates natural language into a sort of intermediate representation you call 'facts'.

This looks like a slot-and-filler language.   This slot-and-filler language is then checked by your Shen program and anomalies

are raised.  The thing is that this slot-and-filler language is not formally specified.

Doing that would clarify the work considerably and it would allow you to do something else - to actually express facts as

a datatype.  This means that some drifts can be typechecked.  This is what I did with plans for ATPs.  Your 'facts' look

ostensibly not complex so you could do that w.o. too much bother.  It would be your decision as to how much of what

your program does is done inside the type checker.  But this would make your work type secure as well as more approachable.

Mark

[Juan Kat]

Thanks for your feedback, Mark.

I’ve implemented your suggested changes:

logicbox GitHub repository

The system has evolved quite a bit from the original idea. I started thinking of it as an argument checker, but it’s turning into something closer to a structural/provenance analysis tool for compressed reasoning and rhetorical bridges.

At this point I’m trying to better understand the theoretical side of what I’m building — especially around logic, inference, semantics, and argument structure.

Is there a book (or set of books) you’d recommend for thinking about these problems more rigorously?