
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...

LEOII
 Referenced in 51 articles
[sw00512]
 well. LEOII 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...

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

MyhillNerode
 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 buildin 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 sketchescompact, 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...

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

Manifold Regularization
 Referenced in 1 article
[sw24840]
 kernel Hilbert spaces to prove new Representer theorems that provide theoretical basis for the algorithms...

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 precomputes a hierarchical representation of models using tightfitting 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 graphbased representation of proofs, and labeled...

Bliksem
 Referenced in 15 articles
[sw21346]
 Bliksem is a firstorder, 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 ... firstorder proving ideas with the simple representation of the hybrid object languag...