package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Rewriting on Terms and Literals

Rewriting is a (relatively) efficient way of computing on terms and literals using rules that come from the input. Each rule is a pair lhs, rhs (left-hand side, right-hand side) that means that objects matching lhs should be rewritten into rhs.

For term rules, lhs and rhs are both terms (with vars rhs ⊆ vars lhs).

For literal rules, lhs is an atomic literal, and rhs is a list of clauses.

This is used for Deduction Modulo in the prover.

type term = Term.t
type defined_cst

Payload of a defined function symbol or type

type proof = Proof.step
val section : Util.Section.t
module Term : sig ... end

Rewriting on Literals and Clauses

module Lit : sig ... end

Rules in General

type rule =
  1. | T_rule of Term.rule
  2. | L_rule of Lit.rule
module Rule : sig ... end
module Rule_set : CCSet.S with type elt = rule
type rule_set = Rule_set.t

Defined Constant

A constant that is defined by at least one rewrite rule

module Defined_cst : sig ... end
val as_defined_cst : ID.t -> defined_cst option
val is_defined_cst : ID.t -> bool
val all_cst : Defined_cst.t Iter.t
val all_rules : Rule.t Iter.t