LEO-II and Satallax on the Sledgehammer test bench

DOI10.1016/j.jal.2012.12.002zbMath1262.68161OpenAlexW2102647770WikidataQ57382576 ScholiaQ57382576MaRDI QIDQ1948289

Jasmin Christian Blanchette, Nik Sultana, Lawrence Charles Paulson

Publication date: 2 May 2013

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2012.12.002

zbMATH Keywords

higher-order logicproof assistantsautomatic theorem provers

Mathematics Subject Classification ID

Related Items

Unnamed Item ⋮ Proofs and Reconstructions ⋮ Unnamed Item ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Internal Guidance for Satallax ⋮ Extending SMT solvers to higher-order logic ⋮ Sledgehammer ⋮ A Knuth-Bendix-like ordering for orienting combinator equations

Uses Software

• LEO-II
• TPS
• Isabelle/HOL
• TPTP
• Metis_
• Satallax
• E Theorem Prover

This page was built for publication: LEO-II and Satallax on the Sledgehammer test bench