• GOLOG

  • Referenced in 173 articles [sw02159]
  • based on a formal theory of action specified in an extended version of the situation...
  • ETPS

  • Referenced in 161 articles [sw06302]
  • prover for first-order logic and type theory. The latter is a cut-down version ... various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive ... Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Second Edition, Kluwer Academic ... ETPS: A System to Help Students Write Formal Proofs (postscript...
  • TPS

  • Referenced in 75 articles [sw00973]
  • prover for first-order logic and type theory. The latter is a cut-down version ... various mathematical activities, promoting development of formal theories in a wide variety of disciplines, deductive...
  • Isabelle/ZF

  • Referenced in 64 articles [sw04973]
  • protocols. Isabelle/ZF formalizes the greater part of elementary set theory, including relations, functions, injections, surjections ... Theorem. Isabelle/ZF also provides theories of lists, trees, etc., for formalizing computational notions. It supports ... cardinality of branching. (ZF: Zermelo-Fraenkel Set Theory...
  • Lean

  • Referenced in 46 articles [sw15148]
  • small trusted kernel based on dependent type theory. It aims to bridge the gap between ... currently being used to formalize category theory, homotopy type theory, and abstract algebra. We describe...
  • LEGO

  • Referenced in 108 articles [sw09685]
  • Calculus of Constructions (GCC) and the Unified Theory of Dependent Types (UTT). LEGO ... more practical by bringing the level of formalization closer to that of informal mathematics ... theories, and the support of specifying new inductive types, provide an expressive language for formalization...
  • JavaFAN

  • Referenced in 32 articles [sw01934]
  • lines of Maude code, specifying formally the semantics of Java and JVM in rewriting logic ... search and LTL model checking of rewriting theories...
  • CeTA

  • Referenced in 47 articles [sw06584]
  • this end, we first formalized the required theory of term rewriting including three major termination...
  • OTTER

  • Referenced in 320 articles [sw02904]
  • Otter is research in abstract algebra and formal logic. Otter and its predecessors have been ... Boolean algebra, logic calculi, combinatory logic, group theory, lattice theory, and algebraic geometry. Note: Otter/Mace2...
  • Oyster

  • Referenced in 34 articles [sw19629]
  • with Oyster. Martin-Löf type theory provides a formal framework for the construction of verified ... both specified and written in the type theory. We describe an implementation of the type...
  • MegaWave

  • Referenced in 27 articles [sw04428]
  • book introduces the reader to a recent theory in Computer Vision yielding elementary techniques ... from and are a mathematical formalization of the Gestalt theory. Gestalt theory, which had never...
  • NESTOR

  • Referenced in 27 articles [sw22096]
  • knowledge-based methods within a formal probability theory framework. A user interface module gives...
  • ForTheL

  • Referenced in 11 articles [sw09797]
  • ForTheL — the language of formal theories. ForTheL, an acronym for “Formal Theory Language...
  • Grail

  • Referenced in 22 articles [sw00374]
  • state machines, regular expressions, and other formal language theory objects. Using Grail, one can input...
  • LFLC 2000

  • Referenced in 12 articles [sw08217]
  • based on deep results obtained in formal theory of fuzzy logic. It makes it possible...
  • MMT

  • Referenced in 52 articles [sw07136]
  • modular mathematical theories. Thus, it provides an interface layer between formally rigorous mathematical systems...
  • FAdo

  • Referenced in 16 articles [sw10335]
  • tools for symbolic manipulation of formal languages. To allow high-level programming with complex data ... pedagogical tool for teaching automata theory and formal languages. For the graphical visualization and interactive...
  • XDuce

  • Referenced in 54 articles [sw12436]
  • theory of regular tree automata, and present a complete formal definition of its core, along...
  • Isabelle/PIDE

  • Referenced in 13 articles [sw07185]
  • math education tools with fully-formal background theories has often been answered negatively ... without obstructing the view on applications of formal methods, formalized mathematics, and math education...
  • MathSAT

  • Referenced in 61 articles [sw09449]
  • theory of bit-vectors. It was explicitly designed for being used in formal verification...