Solving for set variables in higher-order theorem proving

DOI10.1007/3-540-45620-1_33MaRDI QIDQ4809075zbMATH OpenFDO

Authors Chad E. Brown

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2392/23920408.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• On sets, types, fixed points, and checkerboards
• Higher-order positive set constraints
• Reducing higher-order theorem proving to a sequence of SAT problems
• Reducing higher-order theorem proving to a sequence of SAT problems
• Proof search with set variable instantiation in the calculus of constructions

Cited in

(6)

• Reducing higher-order theorem proving to a sequence of SAT problems
• Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
• LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
• Proof search with set variable instantiation in the calculus of constructions
• Types, Tableaus and Gödel’s God in Isabelle/HOL
• TPS: A hybrid automatic-interactive system for developing proofs

Describes a project that uses

Uses Software

• TPS
• Isabelle/ZF

This page was built for publication: Solving for set variables in higher-order theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4809075)