Logtk.Proof.S · logtk 1.6 · OCaml Packages

logtk

Core types and algorithms for logic

Version

Overview Documentation

IN THIS PACKAGE

library logtk
- module Logtk
  - module AllocCache
    
    module Arr
  - module Binder
    
    module TPTP
    
    module ZF
  - module Builtin
    
    module Arith
    
    module ArithOp
    
    module Map
    
    module Set
    
    module TPTP
    
    module Tag
    
    module Tbl
    
    module ZF
  - module Cnf
  - module Comparison
    
    module type PARTIAL_ORD
  - module Compute_prec
  - module Congruence
    
    module FO
    
    module Make
    
    argument 1-T
    
    module type TERM
  - module Congruence_intf
    
    module type S
  - module DBEnv
  - module Defined_pos
    
    module Arr
  - module Dtree
    
    module Default
    
    module Make
    
    argument 1-E
  - module FV_tree
    
    module Make
    
    argument 1-C
    
    module Feature_fun
  - module FeatureVector
    
    module Make
    
    argument 1-C
    
    module Feature
  - module Fingerprint
    
    module Make
    
    argument 1-X
    
    module Leaf
  - module FixpointUnif
  - module Flex_state
  - module HO_unif
  - module HVar
  - module Hash
  - module Hashcons
    
    module type HashedType
    
    module Make
    
    argument 1-X
    
    module MakeNonWeak
    
    argument 1-X
    
    module type S
  - module IArray
  - module ID
    
    module Map
    
    module Set
    
    module Tbl
  - module Ind_ty
  - module Index
    
    module BasicEquation
    
    module MakeLeaf
    
    argument 1-X
  - module Index_intf
    
    module type CLAUSE
    
    module type EQUATION
    
    module type LEAF
    
    module type SUBSUMPTION_IDX
    
    module C
    
    module type TERM_IDX
    
    module Leaf
    
    module type UNIT_IDX
    
    module E
  - module InnerTerm
    
    module DB
    
    module Map
    
    module Pos
    
    module Seq
    
    module Set
    
    module Tbl
    
    module VarMap
    
    module VarSet
    
    module VarTbl
  - module Input_format
  - module Int_lit
    
    module Focus
    
    module Seq
    
    module Util
  - module Interfaces
    
    module type EQ
    
    module type GROUP
    
    module type HASH
    
    module type ITER
    
    module type MONOID
    
    module type ORD
    
    module type PRINT
    
    module type PRINT1
    
    module type PRINT2
    
    module type PRINT3
    
    module type PRINT_DE_BRUIJN
    
    module type PRINT_OVERLOAD
  - module JPFull
    
    module Make
    
    argument 1-S
  - module JP_unif
    
    module S
  - module Lambda
    
    module Inner
  - module LazyList
  - module Literal
    
    module Comp
    
    module Conv
    
    module Pos
    
    module Seq
    
    module Set
    
    module View
  - module Literals
    
    module Conv
    
    module Pos
    
    module Seq
    
    module View
  - module Monome
    
    module Focus
    
    module Int
    
    module Modulo
    
    module Solve
    
    module Rat
    
    module Seq
  - module Multiset
    
    module Make
    
    argument 1-X
    
    module Seq
  - module Multiset_intf
    
    module type S
    
    module Seq
  - module Multisets
    
    module MMT
    
    module Seq
    
    module MT
    
    module Seq
  - module NPDtree
    
    module Make
    
    argument 1-E
    
    module MakeTerm
    
    argument 1-X
    
    module Leaf
  - module Options
  - module Ordering
  - module Ordinal
  - module Output_format
  - module PUnif
    
    module IntSet
    
    module Make
    
    argument 1-S
  - module ParseLocation
    
    module Infix
  - module PatternUnif
    
    module S
  - module Position
    
    module Build
    
    module Map
    
    module With
    
    module Infix
  - module PragUnifParams
  - module Precedence
    
    module Constr
    
    module Seq
    
    module Weight
    
    module Infix
  - module Proof
    
    module Kind
    
    module Parent
    
    module Result
    
    module Rule
    
    module S
    
    module Tbl
    
    module Src
    
    module Step
  - module Rat_lit
    
    module Focus
    
    module Seq
  - module Rewrite
    
    module Defined_cst
    
    module Lit
    
    module Rule
    
    module Rule
    
    module Rule_set
    
    module Term
    
    module Rule
    
    module Rule_inst_set
    
    module Set
  - module SLiteral
    
    module TPTP
    
    module ZF
  - module STerm
    
    module Map
    
    module Seq
    
    module Set
    
    module StrMap
    
    module StringSet
    
    module TPTP
    
    module TPTP_THF
    
    module Tbl
    
    module ZF
  - module Scoped
  - module Signal
  - module Signature
    
    module Seq
  - module Skolem
  - module SolidSubsumption
    
    module Make
    
    argument 1-S
  - module SolidUnif
    
    module Make
    
    argument 1-S
  - module Statement
    
    module Seq
    
    module TPTP
    
    module ZF
  - module Subst
    
    module FO
    
    module Projection
    
    module Renaming
    
    module type SPECIALIZED
    
    module Ty
  - module Term
    
    module AC
    
    argument 1-A
    
    module type AC_SPEC
    
    module Arith
    
    module Classic
    
    module Conv
    
    module DB
    
    module Form
    
    module IntMap
    
    module Map
    
    module Pos
    
    module Seq
    
    module Set
    
    module TPTP
    
    module Tbl
    
    module VarMap
    
    module VarSet
    
    module VarTbl
    
    module ZF
  - module Test_prop
  - module Type
    
    module Conv
    
    module Map
    
    module Seq
    
    module Set
    
    module TPTP
    
    module Tbl
    
    module VarMap
    
    module VarSet
    
    module VarTbl
    
    module ZF
  - module TypeInference
    
    module Ctx
    
    module TyBuiltin
  - module TypedSTerm
    
    module Form
    
    module Map
    
    module Seq
    
    module Set
    
    module Subst
    
    module TPTP
    
    module TPTP_THF
    
    module Tbl
    
    module Ty
    
    module UStack
    
    module Var_tbl
    
    module ZF
  - module Unif
    
    module FO
    
    module Inner
    
    module Ty
  - module UnifFramework
    
    module Make
    
    argument 1-X
    
    module type PARAMETERS
  - module Unif_constr
    
    module FO
  - module Unif_intf
    
    module type S
  - module Unif_subst
    
    module FO
  - module UnionFind
    
    module Make
    
    argument 1-P
    
    module type PAIR
  - module UntypedAST
    
    module A
  - module Util
    
    module Exn
    
    module Flag
    
    module Int_map
    
    module Int_set
    
    module Section
  - module Var
    
    module Set
    
    module Subst
library logtk.parsers
- module Logtk_parsers
  - module Ast_dk
    
    module Map
    
    module Seq
    
    module Set
    
    module StrMap
    
    module StringSet
    
    module TPTP
    
    module TPTP_THF
    
    module Tbl
    
    module ZF
  - module Ast_tptp
  - module CallProver
    
    module Eprover
    
    module Prover
  - module Lex_dk
  - module Lex_tptp
  - module Lex_zf
  - module Parse_dk
  - module Parse_tptp
  - module Parse_zf
  - module Parsing_utils
  - module Tip_ast
  - module Tip_lexer
  - module Tip_parser
  - module Trace_tstp
    
    module StepTbl
  - module Util_dk
  - module Util_tip
  - module Util_tptp
  - module Util_zf
library logtk.proofs
- module Logtk_proofs
  - module LLProof
    
    module Dot
    
    module Tbl
  - module LLProof_check
  - module LLProof_conv
  - module LLProver
  - module LLTerm
    
    module Conv
    
    module Form
    
    module Int_op
    
    module type LINEXP
    
    module Linexp_int
    
    module Linexp_rat
    
    module Rat_op
    
    module Set
library logtk.solving
- module Logtk_solving
  - module Lpo
    
    module Constraint
    
    module Seq
    
    module FO
    
    module Solution
    
    module TypedSTerm

Module Logtk . Proof . S

type t = proof

val result : t -> result

val step : t -> step

val compare : t -> t -> int

val equal : t -> t -> bool

val hash : t -> int

val compare_by_result : t -> t -> int

Compare proofs by their result

module Tbl : CCHashtbl.S with type key = t

Constructors and utils

In all the following constructors, theories defaults to the empty list. Axiom constructors have default role "axiom"

val mk : step -> Result.t -> t

Main constructor

val mk_f : step -> form -> t

val mk_f_trivial : form -> t

val mk_f_by_def : ID.t -> form -> t

val mk_f_inference : rule:rule -> form -> parent list -> t

val mk_f_simp : rule:rule -> form -> parent list -> t

val mk_f_esa : rule:rule -> form -> parent list -> t

val adapt : t -> Result.t -> t

val adapt_f : t -> form -> t

val is_proof_of_false : t -> bool

Conversion to a graph of proofs

val as_graph : ( t, rule * Subst.Projection.t option * infos ) CCGraph.t

Get a graph of the proof

val traverse : ?traversed:unit Tbl.t -> order:[ `BFS | `DFS ] -> t -> t Iter.t

IO

val pp_result_of : t CCFormat.printer

val pp_notrec : t CCFormat.printer

Non recursive printing on formatter

val pp_notrec1 : t CCFormat.printer

Non recursive printing on formatter, including parents

val pp_tstp : t CCFormat.printer

val pp_normal : t CCFormat.printer

val pp_zf : t CCFormat.printer

val pp_in : Options.print_format -> t CCFormat.printer

Prints the proof according to the given input switch

val pp_dot : name:string -> t CCFormat.printer

Pretty print the proof as a DOT graph

val pp_dot_file : ?name:string -> string -> t -> unit

print to dot into a file

val pp_dot_seq : name:string -> t Iter.t CCFormat.printer

Print a set of proofs as a DOT graph, sharing common subproofs

val pp_dot_seq_file : ?name:string -> string -> t Iter.t -> unit

same as pp_dot_seq but into a file