• LTL2BA

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

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

  • Referenced in 146 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 13 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...
  • DELORES

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

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

  • Referenced in 23 articles [sw06872]
  • Theorem Proving in First-Order Logic modulo Linear Integer Arithmetic. Princess is a theorem prover...
  • 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...
  • 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...
  • PESSOA

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

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

  • Referenced in 17 articles [sw07214]
  • symbolic algorithms), partial order reduction and linear temporal logic...
  • 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...
  • Clingcon

  • Referenced in 36 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...
  • linTAP

  • Referenced in 6 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...
  • RoVerGeNe

  • Referenced in 13 articles [sw10954]
  • models, dynamical properties are expressed in linear temporal logic and uncertain parameters are specified...
  • llprover

  • Referenced in 4 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...
  • Datalog LITE

  • Referenced in 10 articles [sw28894]
  • linear-time evaluation, Datalog LITE is highly expressive: It encompasses popular modal and temporal logics ... free portion of guarded fixed-point logic. Consequently, linear-time model checking algorithms ... mentioned logics are obtained in a unified way. The results are complemented by inexpressibility proofs ... effect that linear-time fragments of extit{stratified} Datalog have too limited expressive power...
  • TRP++

  • Referenced in 15 articles [sw14679]
  • theorem prover for Propositional Linear Time Temporal Logic based on the temporal resolution calculus...