gistfile1.mkd

The Rho Computational Logic Toolkit

Summary

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
      • Symbolic constants
      • Numeric constants
        • Integer
        • Float
        • Rational
      • Character strings
      • Variables
  • Predicates
  • Functions
  • Substitutions
• Second-Order Formulas
  • Second-Order, typed variables
    • Formula variables
    • Variable variables
• 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
  • Matching
  • Unification
  • Resolution
  • Paramodulation
  • Subsumption
  • Formula and Theory analysis
  • 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
  • Augmented Perfect Discrimination Tree Index
  • Substitution Tree Index