scientific article; zbMATH DE number 5850143
From MaRDI portal
Publication:3075247
Recommendations
- A Brief Overview of Mizar
- Presenting and explaining Mizar
- Mizar: state-of-the-art and beyond
- A comparison of Mizar and Isar
- Alternative Aggregates in Mizar
- MizAR 40 for Mizar 40
- scientific article; zbMATH DE number 1863397
- The Mizohata complex
- On rewriting rules in Mizar
- Tentative experiments with ellipsis in Mizar
Cited in
(67)- The role of the Mizar mathematical library for interactive proof development in Mizar
- Mizar
- Automating formalization by statistical and semantic parsing of mathematics
- A consistent foundation for Isabelle/HOL
- Flexary connectives in Mizar
- Eliciting implicit assumptions of Mizar proofs by property omission
- Methods of lemma extraction in natural deduction proofs
- ATP and presentation service for Mizar formalizations
- The Mizar Mathematical Library in OMDoc: translation and applications
- On rewriting rules in Mizar
- Custom automations in Mizar
- Improving stateful premise selection with transformers
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- Semantics of Mizar as an Isabelle object logic
- Premise selection for mathematics by corpus analysis and kernel methods
- The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema
- Initial comparison of formal approaches to fuzzy and rough sets
- Accessing the Mizar library with a weakly strict Mizar parser
- Extracting Higher-Order Goals from the Mizar Mathematical Library
- Race against the teens -- benchmarking mechanized math on pre-university problems
- From types to sets by local type definitions in higher-order logic
- Four decades of \textsc{Mizar}. Foreword
- Mechanizing complemented lattices within Mizar type system
- MizAR 40 for Mizar 40
- Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- New Developments in Parsing Mizar
- Checking proofs
- The teaching tool CalcCheck: a proof-checker for Gries and Schneider's ``Logical approach to discrete math
- The Mizohata complex
- A Brief Overview of Mizar
- Formalizing lattice-theoretical aspects of rough and fuzzy sets
- A learning-based fact selector for Isabelle/HOL
- Readable formalization of Euler's partition theorem in Mizar
- Mizar: state-of-the-art and beyond
- Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
- Tools for MML environment analysis
- The Proof Certifier Checkers
- Recycling proof patterns in Coq: case studies
- Learning-assisted theorem proving with millions of lemmas
- Theorem proving in large formal mathematics as an emerging AI field
- Can an A.I. win a medal in the mathematical olympiad? -- Benchmarking mechanized mathematics on pre-university problems
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- Automated Improving of Proof Legibility in the Mizar System
- SAT-enhanced Mizar proof checking
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
- ProofLang: the language of arXiv proofs
- Extending numeric automation for number theory formalizations in Mizar
- Targeted configuration of an SMT solver
- Conway numbers -- formal introduction
- Elementary number theory problems. XII: Primes in arithmetic progression
- Simple extensions
- Symmetrical piecewise linear functions composed by absolute value function
- Integral of continuous functions of two variables
- Solving hard Mizar problems with instantiation and strategy invention
- Remote verification system for Mizar integrated with emwiki
- Higher order partial differentiable functions
- Mechanisation of model-theoretic conservative extension for HOL with ad-hoc overloading
- Stateful premise selection by recurrent neural networks
- Deep reinforcement learning for synthesizing functions in higher-order logic
- How much should this symbol weigh? A GNN-advised clause selection
- The Naproche-ZF theorem prover (short paper)
- A computer-assisted proof of correctness of a marching cubes algorithm
- JEFL: joint embedding of formal proof libraries
- Vampire with a brain is a good ITP hammer
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075247)
