LADR

Library of Automated Deduction Routines

• top_input
• ioutil
• banner
• std_options

• interp

• ivy
• xproofs
• ac_redun
• hints
• backdemod
• paramod
• resolve
• clash
• demod
• flatdemod

• clause_misc
• subsume
• random
• fastparse
• di_tree
• features
• int_code
• weight
• lindex
• maximal
• compress
• sos
• pindex
• parautil
• clausify
• cnf
• just
• clauses
• clauseid
• clist
• topform
• literals
• formula

• attrib
• basic
• mindex
• btm
• btu
• dioph
• discrimw
• discrimb
• discrim
• fpa
• fpalist
• unify

• accanon
• parse
• termorder
• flatterm
• tlist
• listterm
• termflag
• term

• symbols
• options
• glist
• strbuf
• string
• hash
• memory
• ibuffer
• fatal
• nonport
• clock
• order