
TCHR
 Referenced in 4 articles
[sw01345]
 constraint solvers, with tabled logic programming. The framework is easily instantiated with new applicationspecific...

HPILoT
 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 searchtree, 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 objectoriented and logic programming. Most of contemporary software systems are implemented using ... which allows the integration of answer set programming into the objectoriented software development process ... about objectoriented 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 nonground 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 higherorder logic. It reads problems in the TPTP THF format ... controlling the order of sub proof term instantiation. The search is based on backtracking ... 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 generalpurpose 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...