Constructive Symbolic Reinforcement Learning via Intuitionistic Logic and Goal-Chaining Inference

TL;DR

This paper presents a new reinforcement learning framework that uses constructive logical inference and goal-chaining to ensure safe, interpretable, and efficient decision-making without probabilistic trial-and-error.

Contribution

It introduces a symbolic, logic-based reinforcement learning approach that guarantees valid actions through proof construction, contrasting with traditional probabilistic methods.

Findings

Achieves perfect safety with no invalid actions.

Demonstrates efficient convergence compared to Q-learning.

Provides interpretable and verifiable plans in gridworld environments.

Abstract

We introduce a novel learning and planning framework that replaces traditional reward-based optimisation with constructive logical inference. In our model, actions, transitions, and goals are represented as logical propositions, and decision-making proceeds by building constructive proofs under intuitionistic logic. This method ensures that state transitions and policies are accepted only when supported by verifiable preconditions -- eschewing probabilistic trial-and-error in favour of guaranteed logical validity. We implement a symbolic agent operating in a structured gridworld, where reaching a goal requires satisfying a chain of intermediate subgoals (e.g., collecting keys to open doors), each governed by logical constraints. Unlike conventional reinforcement learning agents, which require extensive exploration and suffer from unsafe or invalid transitions, our constructive agent builds a provably correct plan through goal chaining, condition tracking, and knowledge accumulation. Empirical comparison with Q-learning demonstrates that our method achieves perfect safety, interpretable behaviour, and efficient convergence with no invalid actions, highlighting its potential for safe planning, symbolic cognition, and trustworthy AI. This work presents a new direction for reinforcement learning grounded not in numeric optimisation, but in constructive logic and proof theory.