• # 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 non-monotonic (inductive) probabilistic logic programming, our framework mainly targets applications...
• # RGITL

• Referenced in 5 articles [sw13917]
• higher-order 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 Internet-based 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 built-in 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 ... many-sorted first-order logic. Many-sorted first-order logic is a very expressive language ... Manzano in her ”Extensions of first-order logic”) have argued that it can be viewed ... other logics, including higher-order logic. It retains the tractability of first-order logic (completeness...
• # Tecton

• Referenced in 9 articles [sw28905]
• constructing proofs of first-order 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 object-level logic ... second-order 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 first-order 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 first-order logic with several constructs such as inductive definitions, aggregates and arithmetic ... grounders and with grounders for Answer Set Programming...
• # Template-Coq

• Referenced in 3 articles [sw27569]
• Towards certified meta-programming with typed Template-Coq. Template-Coq (url{https://template-coq.github.io/template-coq}) ... 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...