• HARP

  • Referenced in 16 articles [sw26323]
  • more readable by excising redundancies from proof trees. Domain-independent heuristics are formulated to capture ... world knowledge, guide the search for proofs and help eliminate irrelevant premisses...
  • BinaryTrees

  • Referenced in 22 articles [sw14282]
  • equivalent if the respective n-leaf trees that avoid them are equinumerous. We investigate ... equivalence classes combinatorially. Toward establishing bijective proofs of tree pattern equivalence, we develop a general...
  • DDebugger

  • Referenced in 15 articles [sw09904]
  • responsible for the error by building a tree representing this computation and guiding the user ... abbreviation of the proof trees computed with this calculus to build appropriate debugging trees...
  • GF

  • Referenced in 34 articles [sw13667]
  • used both for linearizing syntax trees and parsing strings. GF can describe both formal ... semantic conditions, such as well-typedness and proof obligations. Multilingual grammars, where one abstract syntax ... where syntax trees are constructed in an interactive editor similar to proof editors based...
  • Zeno

  • Referenced in 11 articles [sw07735]
  • Isabelle code. Zeno searches for a proof tree by iteratively reducing the goal into ... definitions, and avoid the repetition of similar proof steps.par We compare with the rippling based...
  • Timbuk

  • Referenced in 47 articles [sw06351]
  • achieving proofs of reachability over Term Rewriting Systems and for manipulating Tree Automata (bottom...
  • KRIPKE

  • Referenced in 8 articles [sw01162]
  • which will contain as a sub-tree a proof of A if there ... exponential rate at which the proof search tree for A usually grows. Hence...
  • XDuce

  • Referenced in 54 articles [sw12436]
  • tree automata, and present a complete formal definition of its core, along with a proof...
  • Isabelle/ZF

  • Referenced in 63 articles [sw04973]
  • main application is the formalization of mathematical proofs and in particular formal verification, which includes ... Theorem. Isabelle/ZF also provides theories of lists, trees, etc., for formalizing computational notions. It supports...
  • R-SATCHMO

  • Referenced in 3 articles [sw06620]
  • atoms in different branches of a proof tree; (3) it summarizes the derived refutations ... complete subtree is constructed in a proof tree. Moreover, R-SATCHMO can be used...
  • Abella

  • Referenced in 52 articles [sw09461]
  • specification logic and allows the development of proofs of properties about specifications. An important characteristic ... logics is that they exploit the λ-tree syntax approach to treating binding in object...
  • MikiBeta

  • Referenced in 1 article [sw09920]
  • general GUI library for visualizing proof trees. System description and demonstration. This paper describes ... library we are developing for visualizing proof trees. Using MikiBeta, one can construct a proof ... tree step by step by selecting a judgement and clicking an inference rule to apply ... necessary to visualize the complete proof tree. To cope with different kinds of proof trees...
  • ProofTool

  • Referenced in 7 articles [sw22201]
  • analysis and transformation of proofs and related tree-like structures, and its implementation is explained ... compared with three other graphical interfaces for proofs...
  • Prooftree

  • Referenced in 1 article [sw17593]
  • Prooftree is a program for proof-tree visualization during interactive proof development in a theorem ... texts are not displayed in the proof tree itself, but they are shown ... sequent symbol. Long proof commands are abbreviated in the tree display, but show ... sequents and proof commands, can be shown in the display below the tree (on single...
  • Holophrasm

  • Referenced in 2 articles [sw30124]
  • Metamath language and explores partial proof trees using a neural-network-augmented bandit algorithm...
  • Whelp

  • Referenced in 15 articles [sw32446]
  • trees. The prototype has been instantiated to the standard library of the Coq proof assistant...
  • MPTP 0.2

  • Referenced in 50 articles [sw02589]
  • remembering (and, if necessary, abstracting from the proof context) the first-order instances that were ... just a XSLT stylesheet translating the XML tree to the TPTP syntax. The problem creation ... machine-learning system trained on previous proofs. In 329 of these cases, the newly discovered...
  • xpe

  • Referenced in 1 article [sw28724]
  • grammar editor that facilitates typesetting proof trees with (TeX). Theorem provers can be called from ... which provides an integrated environment for proof searching and editing, valuable for educational purposes...
  • PeaCoq

  • Referenced in 1 article [sw21573]
  • additionally offers a proof mode called ”Proof Tree” with the following features: preview...