Execution Pragmatics and Solving

The Concept of Pragmatics

In linguistics, "syntax" is the structure of the sentence, "semantics" is the meaning, and Pragmatics is the intent. CNL-PL makes this distinction explicit. A single sentence like "The user is active" can be interpreted in multiple pragmatic modes:

• Query: "Is the user active?" (Returns boolean)
• Assert: "Make the user active." (Updates KB)
• Verify: "Check if the user is active." (Runs proof)
• Plan: "Find a way to make the user active." (Generates actions)

The distinction between Verify and Proof is important. Verify is the user-facing command that returns a boolean (true/false). Proof is the underlying derivation engine that can optionally produce a trace of how the proposition was derived.

The architecture uses distinct "Engines" for each pragmatic mode, all sharing the same compiled KB and Plan IR.

Plan vs Solve

Plan searches for an action sequence that makes a goal true. Solve binds variables to satisfy a constraint without necessarily producing a sequence of actions. Both use the same KB and bitset primitives, but their outputs are different.

Plan:
Command: Plan to achieve all packages delivered.

Solve:
Command: Find a route such that the route is feasible.

Proof vs Explain

Proof answers "is this true?" and can return a derivation. Explain answers "why is this true?" and returns the justification chain for a specific fact.

Command: Verify that every server is encrypted.
Command: Explain why Server_1 is encrypted.

Rules, constraints, and transitions

Rules encode implications, constraints encode boolean conditions, and transitions define state changes for simulation. They compile into plans that share the same primitives.

Rule: A route is valid if the route is feasible.
Rule: When a delay occurs, then the route is delayed.

Actions, preconditions, effects

Action blocks define how planning changes the world: preconditions are checked as boolean plans, and effects translate into KB updates.

Action: assign a driver to a route.
Agent: a dispatcher.
Precondition: a driver is available and the route is unassigned.
Effect: the driver is assigned to the route.

Solving and CSP

The "Solve" pragmatic treats the CNL input as a CSP (Constraint Satisfaction Problem). Instead of checking if a specific fact is true, it searches for a combination of variable assignments that makes the fact true.

For complex problems (like scheduling or resource allocation), the internal engine might delegate to an SMT (Satisfiability Modulo Theories) solver. SMT solvers are powerful backends capable of reasoning about arithmetic, arrays, and bitvectors simultaneously. The CNL compiler translates the high-level Plan IR into the low-level SMT-LIB format required by these solvers.

Search Algorithms (BFS and DAGs)

For "Planning" and "Proof", the system often needs to explore a state space. It uses BFS (Breadth-First Search) to find the shortest path—whether that is the shortest sequence of actions to achieve a goal, or the shortest logical derivation to prove a theorem.

The result of these searches is often represented as a DAG (Directed Acyclic Graph). In a Proof, the DAG represents the justification tree (A implies B implies C). In a Plan, the DAG represents the causal chain of actions. Ensuring these structures are acyclic is critical for preventing infinite loops in reasoning (circular logic).

Dev Ecosystem (API, CI, JSON)

CNL-PL is designed to be embedded. The API allows host applications (written in Node.js, Python, etc.) to instantiate a Session, feed it text, and receive structured results.

All data exchange—ASTs, Plans, and Results—happens via JSON. This standardized serialization format ensures that the compiler and the runtime can be decoupled, or even run on different machines. Finally, the reliability of the entire stack is guaranteed by a rigorous CI (Continuous Integration) pipeline, which runs thousands of "Golden Tests" (defined in DS05) to ensure that a change in the grammar never breaks the logic engine.