Layered map reasoning

DOI10.1016/S1571-0661(04)00147-1zbMath1263.03008MaRDI QIDQ4923516

Andrea Formisano, Marco Temperini, Eugenio Giovanni Omodeo

Publication date: 24 May 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

relation algebrasalgebraic logicset theoryautomatic theorem provingfirst-order theorem prover

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Axiomatics of classical set theory and its fragments (03E30) Cylindric and polyadic algebras; relation algebras (03G15)

Related Items

A graphical representation of relational formulae with complementation, Three-variable statements of set-pairing, Compiling dyadic first-order specifications into map algebra

Uses Software

• OTTER
• Isabelle/ZF

Cites Work

• Relation algebras: Concept of points and representability
• Set theory in first-order logic: Clauses for Gödel's axioms
• Experimenting with Isabelle in ZF set theory
• Set theory for verification. I: From foundations to functions
• \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
• The problem of finding an inference rule for set theory
• Compiling dyadic first-order specifications into map algebra
• Set theory for verification. II: Induction and recursion
• The representation of relational algebras
• Expressing infinity without foundation
• A Finite Axiomatization for Fork Algebras
• Solvable set/hyperset contexts: I. Some decision procedures for the pure, finite case
• Goals and benchmarks for automated map reasoning
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item