Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)

DOI10.1007/s10958-005-0090-6zbMath1101.68834OpenAlexW2073634051MaRDI QIDQ2577589

Tudor Jebelean, Boris Konev

Publication date: 3 January 2006

Published in: Journal of Mathematical Sciences (New York) (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10958-005-0090-6

zbMATH Keywords

witnessing terms in proofs

Mathematics Subject Classification ID

Uses Software

• Theorema

Cites Work

• The number of proof lines and the size of proofs in first order logic
• Towards the automation of set theory and its logic
• The liberalized \(\delta\)-rule in free variable semantic tableaux
• Automated deduction. A basis for applications. Vol. III: Applications
• Toward Mechanical Mathematics
• An improved proof procedure1
• Automatic derivation of the irrationality of \(e\)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)