On rewriting rules in Mizar

DOI10.1007/S10817-012-9261-6zbMATH Open1260.68376OpenAlexW2042059286MaRDI QIDQ1945908FDOQ1945908

Authors: Artur Korniłowicz 

Publication date: 17 April 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-012-9261-6

Recommendations

• Proving and rewriting
• Custom automations in Mizar
• scientific article; zbMATH DE number 1951640
• scientific article; zbMATH DE number 4074536
• Mizar: state-of-the-art and beyond

zbMATH Keywords

natural deductionterm rewritingproof assistantcomputer algebra system\texttt{Mizar}

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Cites Work

• Title not available (Why is that?)
• A Brief Overview of Mizar
• Variations on the Common Subexpression Problem
• Term Rewriting and All That
• Obvious inferences
• Mathematical knowledge management in MIZAR
• Mathematical Knowledge Management
• Fast Decision Procedures Based on Congruence Closure
• Term Rewriting and Applications
• Preliminaries to classical first-order model theory
• An algorithm for reasoning about equality
• Basic first-order model theory in Mizar

Cited In (21)

• Presentation and manipulation of Mizar properties in an Isabelle object logic
• Hammering Mizar by Learning Clause Guidance (Short Paper).
• Multiplication-related classes of complex numbers
• Mechanizing complemented lattices within Mizar type system
• Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
• Improving legibility of formal proofs based on the close reference principle is NP-hard
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Title not available (Why is that?)
• Accessing the Mizar library with a weakly strict Mizar parser
• Enhancement of \textsc{Mizar} texts with transitivity property of predicates
• Flexary connectives in Mizar
• SAT-enhanced Mizar proof checking
• Four decades of \textsc{Mizar}. Foreword
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• On equivalents of well-foundedness. An experiment in MIZAR
• Formalizing lattice-theoretical aspects of rough and fuzzy sets
• Initial comparison of formal approaches to fuzzy and rough sets
• Fermat's little theorem via divisibility of Newton's binomial
• Using and parsing the Mizar language
• Mizar: state-of-the-art and beyond
• Tools for MML environment analysis

Uses Software

• Mizar

This page was built for publication: On rewriting rules in Mizar

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1945908)