Defining functions on equivalence classes

DOI10.1145/1183278.1183280zbMath1367.68254arXiv1907.07591OpenAlexW3122722170MaRDI QIDQ5277759

Lawrence Charles Paulson

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1907.07591

zbMATH Keywords

theorem provingequivalence classesquotients

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Quotients of Bounded Natural Functors, A Formalisation of Finite Automata Using Hereditarily Finite Sets, Let’s Get Physical: Models and Methods for Real-World Security Protocols, Packaging Mathematical Structures, Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, Exploring the structure of an algebra text with locales, Unnamed Item, Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?