MML
From MaRDI portal
Software:19033
No author found.
Related Items (44)
A survey on retrieval of mathematical knowledge ⋮ Automated and Human Proofs in General Mathematics: An Initial Comparison ⋮ MizAR 40 for Mizar 40 ⋮ Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization ⋮ Unnamed Item ⋮ Mining the Archive of Formal Proofs ⋮ A First Class Boolean Sort in First-Order Theorem Proving and TPTP ⋮ 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 ⋮ System Description: E.T. 0.1 ⋮ Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar ⋮ Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics ⋮ A Brief Overview of Mizar ⋮ MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics ⋮ Crystal: Integrating structured queries into a tactic language ⋮ MPTP 0.2: Design, implementation, and initial experiments ⋮ About quotient orders and ordering sequences ⋮ Unnamed Item ⋮ Eliciting implicit assumptions of Mizar proofs by property omission ⋮ ATP and presentation service for Mizar formalizations ⋮ Custom automations in Mizar ⋮ Unnamed Item ⋮ User interaction with the Matita proof assistant ⋮ Integrating searching and authoring in Mizar ⋮ Cauchy mean theorem ⋮ MaLeCoP Machine Learning Connection Prover ⋮ Flexary connectives in Mizar ⋮ MPTP 0.1 - System Description ⋮ Revisions as an Essential Tool to Maintain Mathematical Repositories ⋮ Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings ⋮ Evaluation of Automated Theorem Proving on the Mizar Mathematical Library ⋮ Information Retrieval and Rendering with MML Query ⋮ Machine learning guidance for connection tableaux ⋮ Sine Qua Non for Large Theory Reasoning ⋮ Licensing the Mizar Mathematical Library ⋮ mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library ⋮ Types for Proofs and Programs ⋮ Mathematical Knowledge Management ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Mathematical Knowledge Management ⋮ Mathematical Knowledge Management ⋮ Presenting and Explaining Mizar ⋮ Premise selection for mathematics by corpus analysis and kernel methods
This page was built for software: MML
