Results 1 to 20 of 382
Sort by:

  • NQTHM
  • Referenced in 151 articles [sw07543]
  • integration of a linear arithmetic decision procedure and the addition of a rather primitive facility ... functions in the logic as new proof procedures upon the establishment of their soundness ... using them efficiently as new proof procedures” [in “The correctness problem in computer science...

  • Isar
  • Referenced in 144 articles [sw04599]
  • Isabelle/Pure meta-logic implementation. Theories, theorems, proof procedures etc. may be used interchangeably between Isabelle...

  • HOL
  • Referenced in 591 articles [sw05492]
  • proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish...

  • SATCHMO
  • Referenced in 97 articles [sw06619]
  • model generation, i.e. a bottom-up proof procedure. The prover was given by a small ... Prolog-program, which implements a tableau proof procedure. One restriction is that it requires range...

  • SETHEO
  • Referenced in 122 articles [sw00707]
  • reduction of the input formula, the proof procedure is realized as a WAM, factorization, lemma...

  • HiLog
  • Referenced in 51 articles [sw01580]
  • admits a sound and complete proof procedure. Applications of HiLog are discussed, including DCG grammars...

  • Waldmeister
  • Referenced in 46 articles [sw19568]
  • prover for unit equational logic. Its proof procedure is unfailing Knuth-Bendix completion [BDP89]. Waldmeister ... space. Within that scope, a complete proof object is constructed at run-time. Read more...

  • SCIFF
  • Referenced in 20 articles [sw20513]
  • abductive logic programming proof procedure, also named SCIFF, for reasoning with expectations in dynamic environments ... completeness results of the SCIFF proof procedure, and we demonstrate SCIFF’s possible application...

  • INTOPT_90
  • Referenced in 306 articles [sw04705]
  • constraints (within a box frame). The solution procedures are based on branch and bound, infeasibility ... John conditions and computationally executed proofs of the existence of feasible points generalizing Hansen...

  • HARP
  • Referenced in 16 articles [sw26323]
  • normal form, and combines a proof condensation procedure with explicitly represented, declaratively formulated heuristics ... format congenial to people. The proof condensation procedure makes proof shorter and more readable...

  • Leo-III
  • Referenced in 16 articles [sw18516]
  • systems with a novel agent-based proof procedure. Key goals of the system’s development ... involve parallelism on various levels of the proof search, adaptability for different external specialists...

  • METEOR
  • Referenced in 16 articles [sw26327]
  • based on a linear input resolution procedure. In particular, the WAM architecture ... which is a linear input proof procedure for full first-order logic, similar...

  • Mace4
  • Referenced in 227 articles [sw06905]
  • ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied ... theorem provers, with the prover searching for proofs and Mace4 looking for countermodels...

  • miz3
  • Referenced in 11 articles [sw18631]
  • synthesis of the procedural and declarative styles of interactive theorem proving. We propose a synthesis ... interactive theorem proving: the procedural style (where proofs are scripts of commands, like ... write formal proofs like normal mathematical text – and the procedural style – strong automation and help ... ways in which the procedural and declarative proof styles have been combined before...

  • Eisbach
  • Referenced in 8 articles [sw13077]
  • lacked a means to write automated proof procedures. This can lead to more duplication...

  • Tac
  • Referenced in 7 articles [sw09455]
  • induction and coinduction. Since the automatic proof procedure is structured using focused proofs, its behavior...

  • CVC
  • Referenced in 49 articles [sw09462]
  • procedure for the theories’ union. Subsidiary decision procedures for theories of arrays, inductive datatypes ... ability to produce independently checkable proofs for valid formulas...

  • HOT

  • Referenced in 6 articles [sw13308]
  • calculus which closely corresponds to the proof procedure implemented in HOT. The second part discusses...

  • MleanCoP
  • Referenced in 8 articles [sw21522]
  • source code of the core proof search procedure consists only of a few lines ... logics and outputs a compact prefixed connection proof. An experimental evaluation shows the strong performance...

  • wbs
  • Referenced in 94 articles [sw11110]
  • recommended values of the parameters of the procedure and show that it offers very good ... addition, we provide a new proof of consistency of binary segmentation with improved rates...