Proofs and Explanations

This section focuses on higher-level reasoning outputs: abductive explanations, Craig interpolants, and interactive proof construction. Core reasoning infrastructure such as SRK and unification is documented in Logic and Solving.

• Abduction
  • Introduction to Abduction
  • Abduction in ARIA
  • References
• Interpolant Generation
  • Introduction to Interpolation
  • Interpolant Generation in Aria
  • References
• Interactive Theorem Proving (ITP)
  • Overview
  • Core Components
  • Advanced Features
  • Configuration
  • Bounded Second-Order Decision Procedure (PoC)
  • Installation
  • API Reference