Pages that link to "Item:Q1663215"

The following pages link to The role of the Mizar mathematical library for interactive proof development in Mizar (Q1663215):

Displaying 50 items.

• Isabelle import infrastructure for the Mizar Mathematical Library (Q1798961) (← links)
• Eliciting implicit assumptions of Mizar proofs by property omission (Q1945901) (← links)
• Human-centered automated proof search (Q2069871) (← links)
• Renamings and a condition-free formalization of Kronecker's construction (Q2113831) (← links)
• About graph unions and intersections (Q2113833) (← links)
• Unification of graphs and relations in Mizar (Q2113834) (← links)
• Partial correctness of a Fibonacci algorithm (Q2113835) (← links)
• Grothendieck universes (Q2113837) (← links)
• Formalization of quasilattices (Q2113839) (← links)
• Pappus's hexagon theorem in real projective plane (Q2119545) (← links)
• On weakly associative lattices and near lattices (Q2119547) (← links)
• Ascoli-Arzelà theorem (Q2119549) (← links)
• On primary ideals. I (Q2119550) (← links)
• Some properties of membership functions composed of triangle functions and piecewise linear functions (Q2119552) (← links)
• Real vector space and related notions (Q2119553) (← links)
• Splitting fields (Q2119554) (← links)
• Algorithm NextFit for the bin packing problem (Q2119556) (← links)
• A new export of the Mizar mathematical library (Q2128826) (← links)
• Automatization of ternary Boolean algebras (Q2171519) (← links)
• Duality notions in real projective plane (Q2171520) (← links)
• Finite dimensional real normed spaces are proper metric spaces (Q2171521) (← links)
• Relationship between the Riemann and Lebesgue integrals (Q2171522) (← links)
• Improper integral. I (Q2171523) (← links)
• Prime representing polynomial (Q2171524) (← links)
• Quadratic extensions (Q2171526) (← links)
• The 3-fold product space of real normed spaces and its properties (Q2171527) (← links)
• About graph sums (Q2171528) (← links)
• Improper integral. II (Q2171529) (← links)
• From LCF to Isabelle/HOL (Q2280211) (← links)
• On the intersection of fields \(F\) with \(F[X]\) (Q2305338) (← links)
• Field extensions and Kronecker's construction (Q2305339) (← links)
• Underlying simple graphs (Q2305340) (← links)
• About graph mappings (Q2305341) (← links)
• About vertex mappings (Q2305342) (← links)
• Operations of points on elliptic curve in affine coordinates (Q2305343) (← links)
• AIM loops and the AIM conjecture (Q2305344) (← links)
• Parity as a property of integers (Q2311518) (← links)
• About supergraphs. I (Q2311519) (← links)
• About supergraphs. II (Q2311520) (← links)
• On algebras of algorithms and specifications over uninterpreted data (Q2311521) (← links)
• On an algorithmic algebra over simple-named complex-valued nominative data (Q2311522) (← links)
• An inference system of an extension of Floyd-Hoare logic for partial predicates (Q2311523) (← links)
• Partial correctness of GCD algorithm (Q2311524) (← links)
• Basic Diophantine relations (Q2311525) (← links)
• On two alternative axiomatizations of lattices by McKenzie and Sholander (Q2311528) (← links)
• Arithmetic operations on short finite sequences (Q2311529) (← links)
• Some remarks about product spaces (Q2311530) (← links)
• Binary representation of natural numbers (Q2311531) (← links)
• Continuity of bounded linear operators on normed linear spaces (Q2311532) (← links)
• Pythagorean tuning: pentatonic and heptatonic scale (Q2311533) (← links)