• TCHR

  • Referenced in 4 articles [sw01345]
  • constraint solvers, with tabled logic programming. The framework is easily instantiated with new application-specific...
  • H-PILoT

  • Referenced in 6 articles [sw23305]
  • Instantiation in Local Theory extensions), a program for hierarchical reasoning in extensions of logical theories...
  • TAS

  • Referenced in 11 articles [sw04900]
  • work on technology for transformational proof and program development, as used by window inference calculi ... certain class of theorems in the underlying logic. Our transformation system TAS compiles these rules ... inference or transformational calculus, and can be instantiated to many different ones; three such instantiations...
  • APT

  • Referenced in 3 articles [sw29303]
  • execution of a constraint logic program can be conceptually shown as a search-tree, where ... represents the search space traversed by the program, and has also a direct relationship with ... amount of work performed by the program. The nodes of the tree can be used ... tool which runs constraint logic programs while depicting a (modified) searchtree, keeping at the same...
  • VS3

  • Referenced in 2 articles [sw19492]
  • solvers. VS3 discovers program invariants with arbitrary, but prespecified, quantification and logical structure. The user ... predicates and invariant templates. VS3 automatically finds instantiations of the unknowns in the templates ... used VS3 to automatically verify ∀ ∃ properties of programs and to infer worst case upper bounds...
  • Pirlo

  • Referenced in 4 articles [sw08421]
  • service component ensembles in rewriting logic Programming autonomic systems with massive number of heterogeneous components ... enrich SCEL, a recently introduced language for programming systems with massive numbers of components, with ... show how the methodology can be instantiated by considering the Maude implementation of SCEL...
  • OOASP

  • Referenced in 2 articles [sw13475]
  • OOASP: connecting object-oriented and logic programming. Most of contemporary software systems are implemented using ... which allows the integration of answer set programming into the object-oriented software development process ... about object-oriented software models and their instantiations. Preliminary results of the OOASP application...
  • aleanTAP

  • Referenced in 2 articles [sw09987]
  • theorems and to ask the prover to instantiate non-ground parts of theorems. We present ... into αKanren, an embedding of nominal logic programming in Scheme. We then show...
  • AgsyHOL

  • Referenced in 4 articles [sw13302]
  • theorem prover for higher-order logic. It reads problems in the TPTP THF format ... controlling the order of sub proof term instantiation. The search is based on back-tracking ... been established in Agda, a dependently typed programming language. The theorem prover can output solutions...
  • ACL2

  • Referenced in 279 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

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

  • Referenced in 22 articles [sw00367]
  • GnT is an experimental implementation of the stable...
  • Isabelle

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

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

  • Referenced in 7 articles [sw01343]
  • PLATYPUS: A platform for distributed answer set solving...
  • GraphBase

  • Referenced in 122 articles [sw01555]
  • The Stanford GraphBase is a freely available collection...
  • Ada95

  • Referenced in 289 articles [sw01753]
  • Ada is a structured, statically typed, imperative, wide...
  • ASSAT

  • Referenced in 169 articles [sw02524]
  • ASSAT (Answer Sets by SAT solvers) is a...
  • MEBN

  • Referenced in 15 articles [sw02784]
  • A logic system that integrates First Order Logic...