
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 firstorder logic and type theory. The latter is a cutdown 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 firstorder logic and type theory. The latter is a cutdown 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: ZermeloFraenkel 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. MartinLö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]
 knowledgebased 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 highlevel 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 fullyformal 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 bitvectors. It was explicitly designed for being used in formal verification...