• FOCI

  • Referenced in 61 articles [sw12868]
  • compute quantifier-free 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 data-based 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 free-variable 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 quantifier-free bit-vector formulas into EPR Bit-precise ... polynomial in general, and then showed that solving quantifier-free bit-vector 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 counterexample-guided 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 term-level λ-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 proof-system 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...