
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 bitvectors...

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 nonmonotonic 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 FirstOrder 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 nondeterministic logarithmic...

LTSmin
 Referenced in 17 articles
[sw07214]
 symbolic algorithms), partial order reduction and linear temporal logic...

APNNToolbox
 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 CurryHoward 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 doublenegation 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 highlevel modeling ... Constraints over nonlinear 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 cutfree proof of the given ... sided sequent of firstorder linear logic. Of course, the proof search of linear logic...

Datalog LITE
 Referenced in 10 articles
[sw28894]
 lineartime evaluation, Datalog LITE is highly expressive: It encompasses popular modal and temporal logics ... free portion of guarded fixedpoint logic. Consequently, lineartime model checking algorithms ... mentioned logics are obtained in a unified way. The results are complemented by inexpressibility proofs ... effect that lineartime 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...