
Warmr
 Referenced in 2 articles
[sw37013]
 mining methods from the field of Inductive Logic Programming (ILP) have potential advantages for structural...

BET
 Referenced in 1 article
[sw12109]
 inductive logic programming workbench. Existing ILP (Inductive Logic Programming) systems are implemented in different languages...

PrASP
 Referenced in 2 articles
[sw18512]
 probabilistic logic programming language based on answer set programming (ASP). Besides serving as a research ... software platform for nonmonotonic (inductive) probabilistic logic programming, our framework mainly targets applications...

GENEX
 Referenced in 1 article
[sw00334]
 Inductive Logic Programming (ILP) is a field of research in which logic programs are synthesized...

RGITL
 Referenced in 5 articles
[sw13917]
 higherorder logic. It extends ITL with explicit interleaved programs and recursive procedures. Deduction ... symbolic execution and induction, known from the verification of sequential programs, which are transferred ... concurrent setting with temporal logic. We include an interleaving operator with compositional semantics...

LPL software
 Referenced in 19 articles
[sw04860]
 induction. Advanced chapters include proofs of soundness and completeness for propositional and predicate logic ... logic courses for undergraduates (philosophy, mathematics, and computer science) to a first graduate logic course ... consists of a book, three logic programs, and an Internetbased grading service. The Online...

LPTP
 Referenced in 7 articles
[sw01822]
 theoretical foundations of LPTP, a logic program theorem prover that has been implemented in Prolog ... prove correctness properties of pure Prolog programs that contain negation and builtin predicates like ... call/$n+ 1$. The largest example program that has been verified using LPTP ... formal theory underlying LPTP is the inductive extension of pure Prolog programs. This...

Java+ITP
 Referenced in 8 articles
[sw32259]
 which are then sent to Maude’s Inductive Theorem Prover (ITP) to be discharged ... extensible and modular rewriting logic semantics of programming languages, for which CPS axiomatizations are indeed...

Gallina
 Referenced in 6 articles
[sw27568]
 mathematical theories and to prove specifications of programs. The theories are built from axioms, hypotheses ... functions, predicates and sets. The syntax of logical objects involved in theories is described ... Vernacular. In Coq, logical objects are typed to ensure their logical correctness. The rules implemented ... algorithm are described in Chapter Calculus of Inductive Constructions...

Athena
 Referenced in 10 articles
[sw09967]
 strict and lexically scoped. It encourages a programming style based on function calls and recursion ... manysorted firstorder logic. Manysorted firstorder logic is a very expressive language ... Manzano in her ”Extensions of firstorder logic”) have argued that it can be viewed ... other logics, including higherorder logic. It retains the tractability of firstorder logic (completeness...

Tecton
 Referenced in 9 articles
[sw28905]
 constructing proofs of firstorder logic formulas and of program specifications expressed using formulas ... automating substantial parts of proofs through rewriting, induction, case analysis, and generalization inference mechanisms, along...

evt
 Referenced in 7 articles
[sw09805]
 results of the project “Verification of ERLANG Programs ”, which is funded by the Swedish Business ... formulated as behavioural properties in a modal logic with recursion. We give a summary ... principles essential for successful proofs such as inductive and compositional reasoning, and an efficient treatment ... supporting verification in the presence of program libraries is outlined. EVT is essentially a classical...

SKIL
 Referenced in 2 articles
[sw25433]
 dedicated to program synthesis and implemented in Quintus Prolog. The objectlevel logic ... secondorder constructive logic denoted AF2 which includes induction through the data type definitions ... proof search. These extracted terms are programs following the programming with proofs paradigm, having...

Density Compiler
 Referenced in 6 articles
[sw28659]
 density functions for probability spaces described by programs in a probabilistic functional language. In this ... Together with Isabelle’s code generation for inductive predicates, this yields a fully verified, executable ... modelled directly in the theorem prover’s logic is defined and proved sound. Then, this...

VeriCon
 Referenced in 5 articles
[sw16297]
 concrete counterexample. VeriCon uses firstorder logic to specify admissible network topologies and desired network ... large repertoire of simple core SDN programs. VeriCon is compositional, in the sense that ... handle large programs. To relieve the burden of specifying inductive invariants from the programmer, VeriCon...

GidL
 Referenced in 1 article
[sw23255]
 extension of firstorder logic with several constructs such as inductive definitions, aggregates and arithmetic ... grounders and with grounders for Answer Set Programming...

TemplateCoq
 Referenced in 3 articles
[sw27569]
 Towards certified metaprogramming with typed TemplateCoq. TemplateCoq (url{https://templatecoq.github.io/templatecoq}) ... handle the entire Calculus of Inductive Constructions (CIC), as implemented by Coq, including the kernel ... inductives, and implement a monad for general manipulation of Coq’s logical environment. We demonstrate...

ANSYS
 Referenced in 685 articles
[sw00044]
 ANSYS offers a comprehensive software suite that spans...

ARMS
 Referenced in 65 articles
[sw00048]
 ARMS: an algebraic recursive multilevel solver for general...

ACL2
 Referenced in 283 articles
[sw00060]
 ACL2 is both a programming language in which...