• LTL2BA

  • Referenced in 100 articles [sw10956]
  • algorithm to generate Büchi automata from Linear Time Logic (LTL) formulae. This algorithm generates...
  • MathSAT

  • Referenced in 61 articles [sw09449]
  • equality and uninterpreted functions, difference logic, linear arithmetic, and the theory of bit-vectors...
  • Lolli

  • Referenced in 52 articles [sw40831]
  • language based on a fragment of linear logic. As such it allows the programmer...
  • NQTHM

  • Referenced in 151 articles [sw07543]
  • same authors’ previous book entitled “A computational logic” (1979; Zbl 0448.68020). The truly important changes ... since 1979 are the integration of a linear arithmetic decision procedure and the addition ... theorem prover. The significant changes in the logic itself are the efficient use of functions...
  • Lilac

  • Referenced in 14 articles [sw08983]
  • functional programming language based on linear logic. We take Abramsky’s term assignment for Intuitionistic ... Linear Logic (the linear term calculus) as the basis of a functional programming language. This...
  • Princess

  • Referenced in 28 articles [sw06872]
  • Theorem Proving in First-Order Logic modulo Linear Integer Arithmetic. Princess is a theorem prover...
  • DELORES

  • Referenced in 26 articles [sw05546]
  • most other non-monotonic logics, defeasible logic has linear complexity, allowing DELORES to execute large...
  • SPOT

  • Referenced in 26 articles [sw09473]
  • simple (yet efficient) translation of LTL (linear temporal logic) into TGBA. We then show...
  • HYPROLOG

  • Referenced in 14 articles [sw02743]
  • HYPROLOG: A new logic programming language with assumptions and abduction. We present HYPROLOG, a novel ... Assumptions are a mechanism inspired by linear logic and taken over from Assumption Grammars...
  • PESSOA

  • Referenced in 22 articles [sw20123]
  • specification in a fragment of Linear Temporal Logic that is expressive enough to describe interesting...
  • LMNtal

  • Referenced in 9 articles [sw07312]
  • simple logical interpretation based on intuitionistic linear logic and a flattening technique. This enables ... call LMNtal a hierarchical, concurrent linear logic language...
  • LTSmin

  • Referenced in 21 articles [sw07214]
  • symbolic algorithms), partial order reduction and linear temporal logic...
  • GraphLog

  • Referenced in 32 articles [sw20098]
  • equivalent to stratified linear Datalog, first order logic with transitive closure, and non-deterministic logarithmic...
  • linTAP

  • Referenced in 7 articles [sw11991]
  • multiplicative and exponential fragment of Girards linear logic. It proves the classical validity ... constructing an analytic tableau and ensures the linear validity using prefix unification ... multiplicative, exponential fragment M?LL of linear logic. Based on a prefixed semantic tableau calculus...
  • Clingcon

  • Referenced in 39 articles [sw09892]
  • answer set solver for (extended) constraint normal logic programs. It combines the high-level modeling ... Constraints over non-linear finite integers can be used in the logic programs. The primary...
  • APNN-Toolbox

  • Referenced in 11 articles [sw06976]
  • computational tree logic (CTL) and linear temporal logic (LTL) to consider more general properties...
  • Lolliproc

  • Referenced in 5 articles [sw22624]
  • Lolliproc: to concurrency from classical linear logic via Curry-Howard and control. While many type ... based on the intuitionistic fragment of linear logic have been proposed, applications in programming languages ... full power of linear logic -- including double-negation elimination -- have remained elusive. Meanwhile, linearity ... this paper we connect classical linear logic and concurrent functional programming in the language Lolliproc...
  • TuLiP

  • Referenced in 14 articles [sw20173]
  • software toolbox for receding horizon temporal logic planning. This paper describes TuLiP, a Python-based ... respect to an expressive subset of linear temporal logic (LTL) specifications. TuLiP combines routines...
  • llprover

  • Referenced in 5 articles [sw11993]
  • Linear Logic Prover (llprover). This small program searches a cut-free proof of the given ... sided sequent of first-order linear logic. Of course, the proof search of linear logic...
  • TTM

  • Referenced in 12 articles [sw11997]
  • theorem prover for the Propositional Linear Temporal Logic called PLTL. TTM allows you to test...