Cited in
(only showing first 100 items - show all)- Mathematical Knowledge Management
- Towards Self-verification of HOL Light
- Proceedings of the mathematical knowledge management symposium, Edinburgh, UKNEWLINENovember 25--29, 2003
- Race against the teens -- benchmarking mechanized math on pre-university problems
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Extended Formula Normalization for ε-Retrieval and Sharing of Mathematical Knowledge
- Computer Aided Systems Theory – EUROCAST 2005
- Introduction to Diophantine approximation. II
- Mathematical knowledge representation: semantic models and formalisms
- scientific article; zbMATH DE number 1424017 (Why is no real title available?)
- A user-friendly interface for a lightweight verification system
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- A logical framework combining model and proof theory
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- From types to sets by local type definition in higher-order logic
- Formalizing Scientifically Applicable Mathematics in a Definitional Framework
- The future of logic: foundation-independence
- Intelligent computer mathematics. 11th international conference, AISC 2012, 19th symposium, Calculemus 2012, 5th international workshop, DML 2012, 11th international conference, MKM 2012, systems and projects, held as part of CICM 2012, Bremen, Germany, July 8--13, 2012. Proceedings
- Two over three: a two-valued logic for software specification and validation over a three-valued predicate calculus
- A formalization of the Smith normal form in higher-order logic
- From the universality of mathematical truth to the interoperability of proof systems
- Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
- JEFL: joint embedding of formal proof libraries
- Vampire with a brain is a good ITP hammer
- Dataset description: formalization of elementary number theory in Mizar
- Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
- MMTTeX: connecting content and narration-oriented document formats
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- User interaction with the Matita proof assistant
- Tarski geometry axioms. III
- Main problems of diagrammatic reasoning. I: The generalization problem
- Rings of fractions and localization
- On duplication in mathematical repositories
- A neurally-guided, parallel theorem prover
- A scalable module system
- From types to sets by local type definitions in higher-order logic
- Isabelle formalization of set theoretic structures and set comprehensions
- Interpreting mathematical texts in Naproche-SAD
- Maintaining a library of formal mathematics
- Analysis of algorithms: an example of a sort algorithm
- Relational formal characterization of rough sets
- Math Literate Knowledge Management via Induced Material
- Mathematical knowledge management. Second international conference, MKM 2003, Bertinoro, Italy, February 16--18, 2003. Proceedings
- Veblen hierarchy
- Mathematical knowledge management: MKM 2001. Electronic proceedings of the 1st international workshop, RISC, Schloß Hagenberg, Austria, September 24--26, 2001
- How to write a 21\(^{\text{st}}\) century proof
- About graph unions and intersections
- Formalization of quasilattices
- Grothendieck universes
- Partial correctness of a Fibonacci algorithm
- Renamings and a condition-free formalization of Kronecker's construction
- Unification of graphs and relations in Mizar
- Event-based proof of the mutual exclusion property of Peterson's algorithm
- Propositional linear temporal logic with initial validity semantics
- Summable family in a commutative group
- Topology from neighbourhoods
- Stone lattices.
- Torsion part of \(\mathbb{Z}\)-module
- ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
- Mechanizing complemented lattices within Mizar type system
- Automated search for impossibility theorems in social choice theory: ranking sets of objects
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- scientific article; zbMATH DE number 1507187 (Why is no real title available?)
- Algebraic extensions
- Presenting and explaining Mizar
- scientific article; zbMATH DE number 2222702 (Why is no real title available?)
- Representing model theory in a type-theoretical logical framework
- Ordered rings and fields
- A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
- Formal Representation of Mathematics in a Dependently Typed Set Theory
- A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$
- Finite Groups Representation Theory with Coq
- MathLang Translation to Isabelle Syntax
- Collaborative Interactive Theorem Proving with Clide
- A tale of two set theories
- Algorithm NextFit for the bin packing problem
- On primary ideals. I
- Pappus's hexagon theorem in real projective plane
- Real vector space and related notions
- Some properties of membership functions composed of triangle functions and piecewise linear functions
- Underlying simple graphs
- Object-free definition of categories
- On square-free numbers
- Prime filters and ideals in distributive lattices
- An inference system of an extension of Floyd-Hoare logic for partial predicates
- On algebras of algorithms and specifications over uninterpreted data
- On two alternative axiomatizations of lattices by McKenzie and Sholander
- Partial correctness of GCD algorithm
- scientific article; zbMATH DE number 2154392 (Why is no real title available?)
- A user interface for a mathematical system that allows ambiguous formulae
- EUCLID
- Groups -- additive notation.
- Two axiomatizations of Nelson algebras.
- Management of Change in Declarative Languages
- Dependently Typed Programming Based on Automated Theorem Proving
- The orthogonal projection and the Riesz representation theorem
- On roots of polynomials over \(F[X]/
- Partial correctness of a factorial algorithm
- Partial correctness of a power algorithm
- Combining source, content, presentation, narration, and relational representation
This page was built for software: Mizar
