• GHC

  • Referenced in 43 articles [sw23765]
  • sole additional syntactic construct, guard. Although Guarded Horn Clauses can be classified into the family ... including dataflow languages, Communicating Sequential Processes, and functional languages for multiprocessing. Except for the lack ... efficient implementation of exhaustive solution search for Horn- clause programs. We showed how to automatically...
  • ProVerif

  • Referenced in 41 articles [sw06558]
  • representation of the protocol by Horn clauses. Its main features are: It can handle many ... public-key cryptography (encryption and signatures), hash functions, and Diffie-Hellman key agreements, specified both...
  • BEACON

  • Referenced in 5 articles [sw16742]
  • Horn formula, and integrates state-of-the-art algorithms for solving different function problems...
  • EXPANDER

  • Referenced in 6 articles [sw22715]
  • single Gentzen clauses or sets of guarded Horn clauses (cf. Chapter 2). The system provides ... tactics. It is written in the functional language SML/NJ. EXPANDER executes single inference steps. Each...
  • SYGRAF

  • Referenced in 4 articles [sw21247]
  • Database Style. It is shown how Horn logic programs can be implemented using database techniques ... common approach to deductive databases, function symbols are allowed to appear in programs...
  • Propositional Resolution

  • Referenced in 1 article [sw28841]
  • rule are considered: ordered resolution (with selection functions), positive and negative resolution, semantic resolution ... complete only for clause sets that are Horn- renamable). We also define a concrete procedure...
  • PDE App

  • Referenced in 1 article [sw32482]
  • spatial field and scalar outputs (as a function of frequency) to the PDE App Server ... acoustic-duct PDE Apps: the exponential horn, the expansion chamber, and the toroidal bend...
  • Coq

  • Referenced in 1784 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Isabelle

  • Referenced in 606 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Macaulay2

  • Referenced in 1658 articles [sw00537]
  • Macaulay2 is a software system devoted to supporting...
  • Magma

  • Referenced in 2857 articles [sw00540]
  • Computer algebra system (CAS). Magma is a large...
  • Maple

  • Referenced in 5040 articles [sw00545]
  • The result of over 30 years of cutting...
  • Mathematica

  • Referenced in 5883 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • MiniSat

  • Referenced in 531 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • PARI/GP

  • Referenced in 586 articles [sw00680]
  • PARI/GP is a widely used Computer Algebra System...
  • PLUMP

  • Referenced in 14 articles [sw00718]
  • The joint CSCS-ETH/NEC collaboration in parallel...
  • SageMath

  • Referenced in 1620 articles [sw00825]
  • Sage (SageMath) is free, open-source math software...
  • UMFPACK

  • Referenced in 354 articles [sw00989]
  • An ANSI C code for sparse LU factorization...
  • ML

  • Referenced in 514 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...