• GEOTHER 1.1

  • Referenced in 30 articles [sw02842]
  • order to manipulate and prove the theorem. From the specification, GEOTHER can automatically assign coordinates ... optimal manner; translate the predicate representation of the theorem into an English or Chinese statement...
  • LEO-II

  • Referenced in 51 articles [sw00512]
  • well. LEO-II has been the first theorem prover that supports ... implemented in Objective CAML and its problem representation language is TPTP...
  • Transfer

  • Referenced in 26 articles [sw21009]
  • build a library of operations and theorems about an abstract type, but they want ... proofs in terms of a more concrete representation type, or “raw” type. Earlier work ... packages: the Transfer package for proving theorems, and the Lifting package for defining constants...
  • Lifting

  • Referenced in 26 articles [sw21010]
  • build a library of operations and theorems about an abstract type, but they want ... proofs in terms of a more concrete representation type, or “raw” type. Earlier work ... packages: the Transfer package for proving theorems, and the Lifting package for defining constants...
  • E-KRHyper

  • Referenced in 11 articles [sw21368]
  • KRHyper system is a model generator and theorem prover for first-order logic with equality ... field of knowledge representation. In contrast to most first order theorem provers, it supports features...
  • Myhill-Nerode

  • Referenced in 10 articles [sw28547]
  • formalise in theorem provers. The reason is that natural representations for automata are graphs, matrices ... corresponding reasoning infrastructure comes for free in theorem provers. We show in this paper that...
  • GCLC

  • Referenced in 29 articles [sw00326]
  • GCLC uses a language GC for declarative representation of figures and for storing mathematical contents ... GCLC, there is a build-in geometrical theorem prover which directly links visual and semantical...
  • Dr.Doodle

  • Referenced in 7 articles [sw09975]
  • Dr.Doodle system, an interactive theorem prover that uses diagrammatic representations. The assumption underlying this project...
  • na10

  • Referenced in 47 articles [sw11511]
  • suitable application of Rouché’s theorem. More precisely, an integerq ... necessarily monic, whose zeros and coefficients are representable as floating point numbers ... relative precision allowed by the classical conditioning theorems with 11.1 average iterations. In the worst...
  • Orbital library

  • Referenced in 13 articles [sw05562]
  • oriented representations and algorithms for logic, mathematics, and computer science. It comprises theorem proving, computer...
  • EasyCrypt

  • Referenced in 28 articles [sw09738]
  • cryptographic systems from proof sketches-compact, formal representations of the essence of a proof ... shelf SMT solvers and automated theorem provers, and then compiled into verifiable proofs...
  • AREP

  • Referenced in 9 articles [sw13167]
  • manipulated, rather than equivalence classes of representations as it is done in approaches that ... theorems in a constructively refined form and derive new results on decomposition matrices of representations...
  • MAYA

  • Referenced in 26 articles [sw03423]
  • relies on development graphs as a uniform representation of structured specifications, which enables ... Moreover, Maya allows the integration of different theorem provers to deal with the actual proof...
  • neural-network-states

  • Referenced in 1 article [sw34798]
  • circuit. This is a powerful representation theorem (which was recently obtained with different methods...
  • VIRT

  • Referenced in 2 articles [sw02513]
  • graph algorithms, symbolic processing and knowledge representation, automatic theorem proving. To test the possibilities...
  • OBBTree

  • Referenced in 29 articles [sw33406]
  • polygonal models. It pre-computes a hierarchical representation of models using tight-fitting oriented bounding ... bounding boxes based on a separating axis theorem, which takes less than 200 operations...
  • Grail

  • Referenced in 7 articles [sw24229]
  • automated theorem prover based on proof nets, a graph-based representation of proofs, and labeled...
  • Bliksem

  • Referenced in 15 articles [sw21346]
  • Bliksem is a first-order, resolution based theorem prover, which is written ... benchmark tests compared various datastructures for representating terms, using the operations of unification and matching...
  • HyLoRes

  • Referenced in 7 articles [sw17660]
  • HyLoRes: A Resolution Based Theorem Prover for Hybrid Logics. HyLoRes is a direct resolution prover ... first-order proving ideas with the simple representation of the hybrid object languag...