Search

Automated theorem provers can be modified in order to use external sources of axioms. This was recently searched in combination with saturation based theorem prover SPASS-XDB. It sends queries to external sources and receives answers during its saturation loop. Lean theorem provers are based on semantic tableau calculus. That's why they need to use different approach. An idea that proving is separated from communication is beeing introduced by this work. Prover generetes so called schematic proof which is later checked if it can be filled with external data so the proof can be completed. This work demonstates this idea on modified version of LeanCoP.