\({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
From MaRDI portal
Publication:1319387
DOI10.1007/BF00881874zbMath0802.68133MaRDI QIDQ1319387
Sidney C. Bailin, Dave Barker-Plummer
Publication date: 12 April 1994
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
TPS: A theorem-proving system for classical type theory ⋮ Proof search with set variable instantiation in the Calculus of Constructions ⋮ Layered map reasoning ⋮ The calculus of constructions as a framework for proof search with set variable instantiation ⋮ Set theory for verification. I: From foundations to functions
Cites Work
- Unnamed Item
- A \(\lambda\)-unifiability test for set theory
- Man-machine theorem proving in graph theory
- A relaxation approach to splitting in an automatic theorem prover
- Towards the automation of set theory and its logic
- The problem of finding an inference rule for set theory
- A Human Oriented Logic for Automatic Theorem-Proving
- A Machine-Oriented Logic Based on the Resolution Principle
This page was built for publication: \({\mathcal Z}\)-match: An inference rule for incrementally elaborating set instantiations
