
FOCI
 Referenced in 61 articles
[sw12868]
 compute quantifierfree Craig interpolants for inconsistent pairs (or more generally, sequences) of formulas. This...

DISCOVERER
 Referenced in 56 articles
[sw07719]
 inequalities. Algorithms for quantifier elimination of real closed fields are the general method for those...

f2lp
 Referenced in 10 articles
[sw09898]
 used for computing the general language. Quantifiers are first eliminated and then the resulting quantifier ... also serve as a reasoning engine for general circumscriptive theories. We illustrate...

Tunability
 Referenced in 9 articles
[sw42100]
 define databased defaults and suggest general measures quantifying the tunability of hyperparameters of algorithms...

SQEMA
 Referenced in 39 articles
[sw03056]
 modal formulae, and thus established a very general correspondence and canonical completeness result. SQEMA ... Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided ... downward monotonicity. For the first, and most general, extension SemSQEMA we prove correctness...

HQSpre
 Referenced in 10 articles
[sw28634]
 preprocessor for dependency quantified Boolean formulas (DQBFs). The latter are a generalization of QBFs, resulting...

KeYmaera
 Referenced in 44 articles
[sw03709]
 automating the verification process, KeYmaera implements a generalized freevariable sequent calculus and automatic proof ... complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy...

embed_modal
 Referenced in 4 articles
[sw28304]
 variants of propositional and quantified modal logics. Despite this generality, our approach remains competitive...

DREAM.3D
 Referenced in 16 articles
[sw26984]
 presents a software environment for processing, segmenting, quantifying, representing and manipulating digital microstructure data ... paper discusses the approach to building a generalized representation strategy for digital microstructures...

bv2epr
 Referenced in 7 articles
[sw07142]
 bv2epr: a tool for polynomially translating quantifierfree bitvector formulas into EPR Bitprecise ... polynomial in general, and then showed that solving quantifierfree bitvector formulas...

Bloqqer
 Referenced in 30 articles
[sw09578]
 Blocked clause elimination for QBF. Quantified Boolean formulas (QBF) provide a powerful framework for encoding ... translation to processable QBF encodings is in general not unique and may either introduce variables ... technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural...

EFSMT
 Referenced in 2 articles
[sw19487]
 modern SMT solvers, and generalizes them to quantifier reasoning by counterexampleguided constraint strengthening...

EdgeRewire
 Referenced in 7 articles
[sw40656]
 rewiring: a general framework. Spectral measures have long been used to quantify the robustness ... maximally improve its robustness, as quantified by spectral measures. We focus on modifications based ... interest directly. Notably, extsc{EdgeRewire} is general to accommodate six different spectral measures. Experiments...

Valigator
 Referenced in 3 articles
[sw00994]
 obner basis computation, and quantifier elimination. We present general principles of the implementation and illustrate...

QLGQ
 Referenced in 2 articles
[sw18547]
 Quantifiers in action. Generalized quantification in query, logical and natural languages. The database industry ... extension of the idea of quantifier in FOL. Hence, GQs can be a meaningful extension...

Bedwyr
 Referenced in 22 articles
[sw09460]
 Checking over Syntactic Expressions. Bedwyr is a generalization of logic programming that allows model checking ... using termlevel λbinders and the ∇ quantifier. These features allow reasoning directly on expressions...

GQML
 Referenced in 2 articles
[sw11996]
 general theorem prover for quantified modal logics. The main contribution of this work is twofold ... style, treating the main domain variants of quantified modal logic and dealing with languages where ... light and simple semantical annotations. Such a general proofsystem results from the fusion into...

leanTAP
 Referenced in 40 articles
[sw09985]
 correctness of leanTAP. Next, the author generalizes the sequent calculus to the modal logic ... extended to the case of quantified modal logics as long as the Barcan formula...

CloudSim
 Referenced in 27 articles
[sw10724]
 have different composition, configuration, and deployment requirements. Quantifying the performance of scheduling and allocation policy ... this paper we propose CloudSim: a new generalized and extensible simulation framework that enables seamless...

JIVE
 Referenced in 17 articles
[sw09511]
 Joint and Individual Variation Explained (JIVE), a general decomposition of variation for the integrated analysis ... each data type, and residual noise. JIVE quantifies the amount of joint variation between data...