On rewriting rules in Mizar

DOI10.1007/s10817-012-9261-6zbMath1260.68376OpenAlexW2042059286MaRDI QIDQ1945908

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

zbMATH Keywords

natural deductionterm rewritingcomputer algebra systemproof assistant\texttt{Mizar}

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items

Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ Four decades of {\textsc{Mizar}}. Foreword ⋮ Mechanizing complemented lattices within Mizar type system ⋮ 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 ⋮ Mizar: State-of-the-art and Beyond ⋮ Tools for MML Environment Analysis ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Formalizing Lattice-Theoretical Aspects of Rough and Fuzzy Sets ⋮ Fermat's little theorem via divisibility of Newton's binomial ⋮ Flexary connectives in Mizar ⋮ Initial Comparison of Formal Approaches to Fuzzy and Rough Sets ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ Enhancement of Mizar Texts with Transitivity Property of Predicates ⋮ SAT-Enhanced Mizar Proof Checking ⋮ Multiplication-related classes of complex numbers

Uses Software

• Mizar

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Obvious inferences
• Preliminaries to Classical First Order Model Theory
• A Brief Overview of Mizar
• Fast Decision Procedures Based on Congruence Closure
• Variations on the Common Subexpression Problem
• An algorithm for reasoning about equality
• Term Rewriting and All That
• Mathematical Knowledge Management
• Term Rewriting and Applications