• GHC

  • Referenced in 43 articles [sw23765]
  • Clauses was born from the examination of existing logic programming languages and logic programming ... restriction of a resolution-based theorem prover for Horn-clause sentences. The restriction...
  • MapDE

  • Referenced in 2 articles [sw35022]
  • integrability conditions and for which an existence-uniqueness theorem is available. Once existence is established...
  • HOL-Omega

  • Referenced in 9 articles [sw06581]
  • widely used HOL theorem prover, as an extension of the existing higher order logic...
  • ILTP

  • Referenced in 28 articles [sw00437]
  • platform for testing and benchmarking automated theorem proving (ATP) systems for first-order and propositional ... problems into the input syntax of some existing intuitionistic ATP systems. It also includes information...
  • GROVER

  • Referenced in 2 articles [sw09968]
  • that are beyond the reach of existing theorem-proving systems operating without such guidance...
  • ELAN

  • Referenced in 108 articles [sw02179]
  • purpose is to support the design of theorem provers, logic programming languages, constraints solvers ... application. This is in contrast to many existing rewriting-based languages where the term reduction...
  • Secondary Sylow

  • Referenced in 3 articles [sw29536]
  • formal proofs: Secondary Sylow Theorems. These theories extend the existing proof of the first Sylow...
  • navierstokes

  • Referenced in 8 articles [sw40625]
  • general method to obtain constructive proofs of existence of periodic orbits in the forced autonomous ... Newton-Kantorovich theorem is applied to obtain the (computer-assisted) proofs of existence. The required...
  • Monotonox

  • Referenced in 4 articles [sw10406]
  • unsorted logic, but most existing highly-efficient automated theorem provers solve problems only in unsorted...
  • jStar

  • Referenced in 32 articles [sw11261]
  • automatic verification system, called jStar, which combines theorem proving and abstract interpretation techniques. We demonstrate ... they have been highly challenging for existing object-oriented verification techniques...
  • DeepMath

  • Referenced in 11 articles [sw27551]
  • sequence models for premise selection in automated theorem proving, one of the main bottlenecks ... while avoiding the hand-engineered features of existing state-of-the-art models ... time deep learning has been applied to theorem proving on a large scale...
  • DefunT

  • Referenced in 1 article [sw32315]
  • proofs for recursive definitions by mining existing termination theorems...
  • Mtac

  • Referenced in 14 articles [sw13075]
  • large scale interactive proof development. However, existing languages for automation via tactics either (a) provide ... within the base logic of the accompanying theorem prover, or (b) rely on advanced type...
  • MathWeb

  • Referenced in 18 articles [sw10293]
  • other fields to find information about theorem prover software, to decide which system is best ... problems, so that, more often than not, existing reasoning procedures are re-implemented instead...
  • disproots

  • Referenced in 4 articles [sw22276]
  • residue theorem. Although several implementations of the argument principle already exist, ours has several advantages...
  • Bliksem

  • Referenced in 15 articles [sw21346]
  • Bliksem is a first-order, resolution based theorem prover, which is written ... less memory. In that time, there existed only one prover using flatterms (Waldmeister), and this...
  • ArcAngelC

  • Referenced in 6 articles [sw06338]
  • application in the formalisation of an existing strategy for verification of Ada implementations of control ... also discuss its mechanisation in a theorem prover, ProofPower...
  • GenerateUHG

  • Referenced in 5 articles [sw26974]
  • work of Royle, we show that there exist nearly cubic 1H graphs of order ... This gives the strongest form of a theorem of Entringer and Swart, and sheds light ... which cubic 3H triangle-free graphs exist. We verify up to order 48 Cantoni...
  • FRIP

  • Referenced in 5 articles [sw14894]
  • overcome a few limitations associated with existing systems. To do this, we propose adaptive circular ... segmentation, which are based on both Bayes’ theorem and texture distribution of image. In addition...