Advertisement
Published in:
2012 | OriginalPaper | Chapter
A Complete Logical System for the Equality of Recursive Terms for Sets
Authors : Lawrence S. Moss, Erik Wennstrom, Glen T. Whitney
Published in: Logic and Program Semantics
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
This paper presents a sound and complete logical system whose atomic sentences are the equalities of recursive terms involving sets. There are two interpretations of this language: one makes use of non-wellfounded sets with finite transitive closure, and the other uses pointed finite graphs modulo bisimulation. Our logical system is a sequent-style deduction system. The main axioms and inference rules come from the
$\mbox{{\it FLR}$_0$}$
-proof system from [6], including the Recursion Inference Rule (but an additional axiom is needed), and also axioms corresponding to the extensionality axiom of set theory.