Flexary connectives in Mizar

DOI10.1016/J.CL.2015.07.002zbMath1387.68207OpenAlexW1625130818MaRDI QIDQ1749141

Artur Korniłowicz

Publication date: 15 May 2018

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.cl.2015.07.002

zbMATH Keywords

ellipsisproof assistantMizarflexary conjunctionflexary disjunction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (9)

Four decades of {\textsc{Mizar}}. Foreword ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Computer Certification of Generalized Rough Sets Based on Relations ⋮ Elementary number theory problems. II ⋮ Elementary number theory problems. VII ⋮ Elementary number theory problems. VIII ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ Enhancement of Mizar Texts with Transitivity Property of Predicates ⋮ Semantics of Mizar as an Isabelle object logic

Uses Software

• Coq
• Isar
• Mizar
• HOL Light
• MML
• OMDoc
• MMode
• Logic2CNF

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• Pseudo-canonical formulae are classical
• Proth numbers
• Obvious inferences
• Triple dots in a formal language
• A compendium of continuous lattices in MIZAR
• ATP and presentation service for Mizar formalizations
• The Mizar Mathematical Library in OMDoc: translation and applications
• On rewriting rules in Mizar
• Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
• Formalization of the Data Encryption Standard
• Abstract matrices in symbolic computation
• A Brief Overview of Mizar
• On a Practical Way of Describing Formal Deductions
• On the Structure of Mizar Types
• Licensing the Mizar Mathematical Library
• Efficient Rough Set Theory Merging
• Automated Discovery of Properties of Rough Sets
• Flexary Operators for Formalized Mathematics
• SAT-Enhanced Mizar Proof Checking
• Types for Proofs and Programs
• Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking
• Mathematical Knowledge Management

This page was built for publication: Flexary connectives in Mizar