nsaspy/prolog-rlm

Fork 0

[RESEARCH][logic-profile] Define a Datalog-safe Prolog reasoning profile using tabling, WFS, and bounded incremental semantics #389

New issue

Open

opened 2026-09-08 01:29:17 +00:00 by nsaspy · 0 comments

nsaspy commented

2026-09-08 01:29:17 +00:00

Owner

Related: #388 #392 #394 #398 #400

Research question

Define the smallest useful Datalog-like profile inside Prolog-RLM so callers can get predictable, explainable, bounded symbolic reasoning without introducing Clojure, Datomic, or a separate Datalog runtime by default.

This is a research/design issue only. Do not implement the profile here.

Motivation

The semantic compiler and Machine Spirit work need a reasoning tier where:

validated semantic records
        ↓
restricted declarative rules
        ↓
query / fixed-point inference
        ↓
provenance + bounded explanation

is safe and operationally predictable.

The profile should use Prolog as the host language while explicitly restricting the accepted rule fragment.

Core research questions

What exact fragment should v1 admit?
- function-free Horn clauses;
- range-restricted/safe variables;
- finite ground extensional domain where required;
- stratified negation and/or tabled Well-Founded Semantics;
- explicit negation separate from negation-as-failure;
- aggregates only if a bounded deterministic semantics is available;
- no arbitrary meta-calls, cuts, side effects, dynamic code loading, or unbounded term construction.
How closely should the profile correspond to classical Datalog, and where should it deliberately differ because SWI-Prolog provides stronger useful semantics?
Which SWI-Prolog primitives are appropriate:
- tabling;
- tnot/1 / WFS;
- incremental tabling;
- monotonic/incremental dynamic predicates where applicable;
- answer subsumption where safe;
- CLP(FD)/CLP(Q/R) as separate trusted profiles rather than pretending they are ordinary Datalog?
What static validation can prove a package belongs to the profile before execution?
What termination/complexity guarantees can honestly be documented per admitted sub-profile?
How should recursive rules, mutually recursive SCCs, negation cycles, and resource exhaustion be reported?
How should proposition/assertion/context identity from #392 map into the rule layer without flattening attribution or provenance?
How should reasoning receipts expose premises, rule IDs, source assertion IDs, profile/version, and unresolved residual conditions?
How should retraction/source withdrawal invalidate tabled/derived answers?
When is SWI incremental tabling sufficient, and when would XSB, Soufflé, ASP, or another engine be materially better?

Candidate profile family

Evaluate at least these candidates instead of pretending one profile fits all semantics:

ground_fact
function_free_horn
stratified_datalog
well_founded_tabled
incremental_horn
trusted_clpfd
trusted_clpqr
preservation_only_quantified

The final design may merge or rename them, but capability promises must remain explicit.

Rule safety contract

Research a validator that rejects or preserves-as-data constructs such as:

arbitrary call/1
consult/1 from semantic input
assert/retract inside knowledge rules
cut / once as semantic truth machinery
unbounded compound-term generation
side effects
foreign predicates without trusted admission
impure built-ins
unsafe variables
unsupported negation cycles

Unknown domain relation names remain inert semantic vocabulary until admitted through the profile/signature layer.

Incremental semantics

Study whether a rule/profile declaration can expose incremental capability equivalent to:

:- table derived/2 as incremental.

without making incremental tabling canonical truth.

Required conceptual invariant:

same canonical semantic input cut + same profile
=> from-scratch result == incrementally maintained result

under normalized answers/receipts.

Research:

dependency-directed invalidation;
assertion addition;
retraction/withdrawal;
supersession;
source validity-time changes;
profile/schema generation changes;
table invalidation after external semantic-ledger updates;
memory/CPU behavior for large recursive closures.

Datalog interoperability

Determine whether Prolog-RLM should expose a clean import/export compatibility lane for actual Datalog syntax/engines while keeping Prolog native.

Compare at least:

ISO/SWI Prolog restricted clauses;
Soufflé-style Datalog;
XSB tabled Prolog;
ASP/stable-model tooling where semantics differ materially;
RDF/SPARQL rule projections only as interoperability, not canonical semantics.

The conclusion may be that no extra runtime is needed for v1.

Required outputs

Produce a research record with:

exact admitted syntax/semantic matrix;
static-safety validation rules;
termination/decidability claims with caveats;
SWI tabling/WFS/incremental capability analysis;
alternative-engine comparison;
provenance/explanation contract;
incremental invalidation model;
adversarial examples;
benchmark plan;
recommended v1 profile(s);
concrete amendments to #392/#394 if needed.

Acceptance

Datalog is treated as a restricted logic-programming profile, not a required separate ecosystem.
Explicit negation remains distinct from NAF/unknown.
Accepted rules cannot perform arbitrary side effects or meta-execution.
Static profile validation is specified before execution.
Recursion/negation/resource exhaustion produce typed outcomes rather than first-found truth.
From-scratch vs incremental semantic equivalence oracle is specified.
Provenance/justification survives rule evaluation.
Recommendation says exactly when SWI alone is sufficient and when another engine is justified.

Non-goals

no Clojure dependency;
no Datomic dependency;
no claim that full Prolog is Datalog;
no arbitrary generated Prolog execution;
no replacement for #400 epistemic-profile research;
no implementation in this issue.

Related: #388 #392 #394 #398 #400 ## Research question Define the smallest useful **Datalog-like profile inside Prolog-RLM** so callers can get predictable, explainable, bounded symbolic reasoning without introducing Clojure, Datomic, or a separate Datalog runtime by default. This is a **research/design issue only**. Do not implement the profile here. ## Motivation The semantic compiler and Machine Spirit work need a reasoning tier where: ```text validated semantic records ↓ restricted declarative rules ↓ query / fixed-point inference ↓ provenance + bounded explanation ``` is safe and operationally predictable. The profile should use Prolog as the host language while explicitly restricting the accepted rule fragment. ## Core research questions 1. What exact fragment should v1 admit? - function-free Horn clauses; - range-restricted/safe variables; - finite ground extensional domain where required; - stratified negation and/or tabled Well-Founded Semantics; - explicit negation separate from negation-as-failure; - aggregates only if a bounded deterministic semantics is available; - no arbitrary meta-calls, cuts, side effects, dynamic code loading, or unbounded term construction. 2. How closely should the profile correspond to classical Datalog, and where should it deliberately differ because SWI-Prolog provides stronger useful semantics? 3. Which SWI-Prolog primitives are appropriate: - tabling; - `tnot/1` / WFS; - incremental tabling; - monotonic/incremental dynamic predicates where applicable; - answer subsumption where safe; - CLP(FD)/CLP(Q/R) as separate trusted profiles rather than pretending they are ordinary Datalog? 4. What static validation can prove a package belongs to the profile before execution? 5. What termination/complexity guarantees can honestly be documented per admitted sub-profile? 6. How should recursive rules, mutually recursive SCCs, negation cycles, and resource exhaustion be reported? 7. How should proposition/assertion/context identity from #392 map into the rule layer without flattening attribution or provenance? 8. How should reasoning receipts expose premises, rule IDs, source assertion IDs, profile/version, and unresolved residual conditions? 9. How should retraction/source withdrawal invalidate tabled/derived answers? 10. When is SWI incremental tabling sufficient, and when would XSB, Soufflé, ASP, or another engine be materially better? ## Candidate profile family Evaluate at least these candidates instead of pretending one profile fits all semantics: ```text ground_fact function_free_horn stratified_datalog well_founded_tabled incremental_horn trusted_clpfd trusted_clpqr preservation_only_quantified ``` The final design may merge or rename them, but capability promises must remain explicit. ## Rule safety contract Research a validator that rejects or preserves-as-data constructs such as: ```text arbitrary call/1 consult/1 from semantic input assert/retract inside knowledge rules cut / once as semantic truth machinery unbounded compound-term generation side effects foreign predicates without trusted admission impure built-ins unsafe variables unsupported negation cycles ``` Unknown domain relation names remain inert semantic vocabulary until admitted through the profile/signature layer. ## Incremental semantics Study whether a rule/profile declaration can expose incremental capability equivalent to: ```prolog :- table derived/2 as incremental. ``` without making incremental tabling canonical truth. Required conceptual invariant: ```text same canonical semantic input cut + same profile => from-scratch result == incrementally maintained result ``` under normalized answers/receipts. Research: - dependency-directed invalidation; - assertion addition; - retraction/withdrawal; - supersession; - source validity-time changes; - profile/schema generation changes; - table invalidation after external semantic-ledger updates; - memory/CPU behavior for large recursive closures. ## Datalog interoperability Determine whether Prolog-RLM should expose a clean import/export compatibility lane for actual Datalog syntax/engines while keeping Prolog native. Compare at least: - ISO/SWI Prolog restricted clauses; - Soufflé-style Datalog; - XSB tabled Prolog; - ASP/stable-model tooling where semantics differ materially; - RDF/SPARQL rule projections only as interoperability, not canonical semantics. The conclusion may be that no extra runtime is needed for v1. ## Required outputs Produce a research record with: - exact admitted syntax/semantic matrix; - static-safety validation rules; - termination/decidability claims with caveats; - SWI tabling/WFS/incremental capability analysis; - alternative-engine comparison; - provenance/explanation contract; - incremental invalidation model; - adversarial examples; - benchmark plan; - recommended v1 profile(s); - concrete amendments to #392/#394 if needed. ## Acceptance - [ ] Datalog is treated as a restricted logic-programming profile, not a required separate ecosystem. - [ ] Explicit negation remains distinct from NAF/unknown. - [ ] Accepted rules cannot perform arbitrary side effects or meta-execution. - [ ] Static profile validation is specified before execution. - [ ] Recursion/negation/resource exhaustion produce typed outcomes rather than first-found truth. - [ ] From-scratch vs incremental semantic equivalence oracle is specified. - [ ] Provenance/justification survives rule evaluation. - [ ] Recommendation says exactly when SWI alone is sufficient and when another engine is justified. ## Non-goals - no Clojure dependency; - no Datomic dependency; - no claim that full Prolog is Datalog; - no arbitrary generated Prolog execution; - no replacement for #400 epistemic-profile research; - no implementation in this issue.

nsaspy referenced this issue

2026-09-08 01:29:20 +00:00

[EPIC][artifact-synthesis] Typed symbolic artifact generation, validation, and repair substrate #407

nsaspy referenced this issue

2026-09-08 01:29:20 +00:00

[EPIC][symbolic-port] Private-source semantics → public symbolic expert/rule corpus #408

nsaspy referenced this issue

2026-09-08 01:46:59 +00:00

[EPIC][cyber-harness] Generic Prolog-RLM cyber reasoning harness for Hackmode/Hackpert #409