gistfile1.mkd

The Rho Computational Logic Toolkit

Overview

The Rho Computational Toolkit is a collection of Scala / JVM APIs that facilitate writing software for an open-ended variety of logical inference programs.

Components

• First-Order Logic Representations
  • Formulas
    • Quantifed
    • Boolean
    • Atomic
    • Equations
    • Clausal
  • Terms
    • Complex (function applications)
    • Simple (constants, variables
  • Predicates
  • Functions
  • Substitutions
• I/O
  • CLIF, the Common Logic Interchange Format
  • Prover9
  • TPTP
  • Rho native format, including notations for clauses, substitutions, second-order formulas, etc.
  • LaTeX (output only)
• Content Management
  • Hierarchical Content TOCs
  • GPT+X (Goal, Problem, Theory + Extra Theories) model of logical problems
• Algorithms
  • Formula and Theory analysis
  • Matching
  • Unification
  • Resolution
  • Paramodulation
  • Subsumption
  • Formula Transformations / Normalizations
    • Various Normal Forms
    • Brand's Transforms
  • SAT
  • Term Ordering
    • Multiset
    • Recursive Path
    • Lexicographic Path
    • Knuth Bendix
  • Term Rewriting
    • Huet's Completion
• Data Structures
  • Perfect Discrimination Tree Index
  • Substitution Tree Index