• Isabelle/HOL

  • Referenced in 945 articles [sw01569]
  • expressed in a formal language and provides tools for proving those formulas in a logical...
  • Isabelle

  • Referenced in 606 articles [sw00454]
  • expressed in a formal language and provides tools for proving those formulas in a logical...
  • Kronos

  • Referenced in 261 articles [sw01270]
  • correctness requirements are expressed in the real-time temporal logic TCTL...
  • SLMC

  • Referenced in 71 articles [sw04604]
  • against dynamical spatial logic specifications. The Spatial Logic Model Checker is a tool for verifying ... safety, liveness, and structural properties expressed in the spatial logic for concurrency of Caires...
  • PROMELA

  • Referenced in 30 articles [sw07635]
  • interactions in distributed systems, and for expressing logical correctness requirements about such interactions. The model...
  • ELAN

  • Referenced in 108 articles [sw02179]
  • support the design of theorem provers, logic programming languages, constraints solvers and decision procedures ... these primitives, more complex strategies can be expressed. In addition the user can introduce ... provides both the logical framework in which deduction systems can be expressed and combined...
  • ITP

  • Referenced in 31 articles [sw09808]
  • development of specifications. Membership equational logic is an expressive version of equational logic, particularly adequate...
  • MiniML

  • Referenced in 46 articles [sw29625]
  • based on the intuitionistic modal logic S4 provides an expressive framework for specifying and analyzing...
  • Boolector

  • Referenced in 27 articles [sw00085]
  • problem of deciding satisfiability of a logical formula, expressed in a combination of first-order...
  • DELORES

  • Referenced in 25 articles [sw05546]
  • chaining reasoning engine for defeasible logic, a less-expressive but more efficient non-monotonic logic...
  • jContractor

  • Referenced in 10 articles [sw01488]
  • rich set of syntactic constructs for expressing contracts without extending the Java language or runtime ... These constructs include support for predicate logic expressions, and referencing entry values of attributes...
  • CEL

  • Referenced in 15 articles [sw12477]
  • supported description logic EL+ offers a selected set of expressive means that are tailored towards ... some idea about what logical aspects can be expressed in CEL ontologies, look...
  • GEOTHER 1.1

  • Referenced in 30 articles [sw02842]
  • into a first-order logical formula, or into algebraic expressions; draw one or several diagrams...
  • NP Datalog

  • Referenced in 9 articles [sw13446]
  • 𝒩𝒫𝒟atalog: A logic language for expressing 𝒩𝒫 search and optimization problems. This paper presents ... logic language for expressing 𝒩𝒫 search and optimization problems. Specifically, first a language obtained ... easy formulation of problems, expressed by means of a declarative logic language, with the efficiency...
  • MSO_Regex_Equivalence

  • Referenced in 7 articles [sw32230]
  • Based on Derivatives of Regular Expressions. Monadic second-order logic on finite ... words (MSO) is a decidable yet expressive logic into which many decision problems ... based on automata but on regular expressions. Decision procedures for regular expression equivalence have been...
  • CP-logic

  • Referenced in 17 articles [sw06947]
  • probabilistic logic programs: we can say precisely which knowledge such a program expresses, in terms ... methodology for probabilistic logic programs, by showing how they can express probabilistic causal laws...
  • PESSOA

  • Referenced in 18 articles [sw20123]
  • fragment of Linear Temporal Logic that is expressive enough to describe interesting properties but simple...
  • EVC

  • Referenced in 8 articles [sw13374]
  • Uninterpreted Functions and Memories (EUFM). The logic expresses connectness of high-level microprocessors. We present...
  • Bedwyr

  • Referenced in 21 articles [sw09460]
  • Model Checking over Syntactic Expressions. Bedwyr is a generalization of logic programming that allows model...
  • JProver

  • Referenced in 12 articles [sw09978]
  • engine in interactive proof assistants with expressive constructive logics. This paper gives a brief overview...