scientific article
From MaRDI portal
Publication:3075247
zbMath1211.68369MaRDI QIDQ3075247
Adam Naumowicz, Adam Grabowski, Artur Korniłowicz
Publication date: 10 February 2011
Full work available at URL: http://jfr.cib.unibo.it/article/view/1980
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema ⋮ Improving stateful premise selection with transformers ⋮ 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 ⋮ JEFL: joint embedding of formal proof libraries ⋮ Vampire with a brain is a good ITP hammer ⋮ 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 ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ The Proof Certifier Checkers ⋮ New Developments in Parsing Mizar ⋮ A learning-based fact selector for Isabelle/HOL ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Checking Proofs ⋮ Automating formalization by statistical and semantic parsing of mathematics ⋮ ProofLang: the language of arXiv proofs ⋮ Extending numeric automation for number theory formalizations in Mizar ⋮ Targeted configuration of an SMT solver ⋮ 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 ⋮ Recycling proof patterns in Coq: case studies ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1 ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper). ⋮ Formalizing Lattice-Theoretical Aspects of Rough and Fuzzy Sets ⋮ A consistent foundation for Isabelle/HOL ⋮ Flexary connectives in Mizar ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Formalization of the fundamental group in untyped set theory using auto2 ⋮ Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck} ⋮ mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library ⋮ 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 ⋮ Mizar ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math” ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Automated Improving of Proof Legibility in the Mizar System ⋮ SAT-Enhanced Mizar Proof Checking ⋮ Premise selection for mathematics by corpus analysis and kernel methods
Uses Software
