• IMPS

  • Referenced in 50 articles [sw09143]
  • specification and inference are performed relative to axiomatic theories, which can be related...
  • Lean

  • Referenced in 37 articles [sw15148]
  • interaction and the construction of fully specified axiomatic proofs. Lean is an ongoing and long...
  • Ynot

  • Referenced in 35 articles [sw12334]
  • types for imperative programs. We describe an axiomatic extension to the Coq proof assistant, that...
  • Darwin

  • Referenced in 25 articles [sw04175]
  • calculus, it is instead automatically axiomatized for a given problem. Darwin is a decision procedure...
  • Separoids

  • Referenced in 20 articles [sw08819]
  • Conditional Independence and Irrelevance. We introduce an axiomatic definition of a mathematical structure that...
  • Checkfence

  • Referenced in 19 articles [sw09939]
  • specify the desired memory model in an axiomatic format. If a test fails, CheckFence provides...
  • MBase

  • Referenced in 17 articles [sw08724]
  • found the whole knowledge base in axiomatic set theory. The viability of this approach...
  • HoTT

  • Referenced in 13 articles [sw15147]
  • formalization of the basic type formers, some axiomatic higher inductive types including the circle...
  • Coquelicot

  • Referenced in 12 articles [sw11552]
  • systems. The Coq system comes with an axiomatization of standard real numbers and a library...
  • KRIPKE

  • Referenced in 8 articles [sw01162]
  • given Hilbert-style axiomatizations and are studied in detail in [1]. By dropping the axioms ... extensional connectives ^ and v from the axiomatizations of these logics we obtain their implication/negation fragments...
  • Tecton

  • Referenced in 9 articles [sw28905]
  • specifications expressed using formulas in Hoare’s axiomatic proof formalism. It is designed to make...
  • UMM

  • Referenced in 8 articles [sw10132]
  • also compare our operational specification style with axiomatic specification styles and explore a mechanism that...
  • Java+ITP

  • Referenced in 8 articles [sw32259]
  • semantics of programming languages, for which CPS axiomatizations are indeed very useful, to develop similarly...
  • LPTP

  • Referenced in 7 articles [sw01822]
  • that the inductive extension is an adequate axiomatization of the operational semantics of pure Prolog...
  • AxiomCalc

  • Referenced in 7 articles [sw20253]
  • AxiomCalc that takes as input any suitable axiomatic extension of Monoidal T-norm Logic...
  • Kleene Algebra

  • Referenced in 7 articles [sw32203]
  • algebras and their most important models as axiomatic type classes in Isabelle/HOL. Kleene algebras...
  • Aximo

  • Referenced in 4 articles [sw15031]
  • Aximo: Automated Axiomatic Reasoning for Information Update. Aximo is a software written in C++ that ... tool is based on the algebraic axiomatics of Dynamic Epistemic Logic. We also present...
  • ConsRank

  • Referenced in 3 articles [sw25204]
  • Ranking(s) According to the Kemeny’s Axiomatic Approach. Compute the median ranking according ... Kemeny’s axiomatic approach. Rankings can or cannot contain ties, rankings can be both complete...
  • PLM

  • Referenced in 3 articles [sw38031]
  • mathematics, as abstract objects and provides an axiomatic framework that allows to reason about these ... metaphysical theory that can be used to axiomatize and describe a wide range of philosophical...