On rewriting rules in Mizar
From MaRDI portal
Publication:1945908
DOI10.1007/s10817-012-9261-6zbMath1260.68376OpenAlexW2042059286MaRDI QIDQ1945908
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
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
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
