Extensional paramodulation for higher-order logic and its effective implementation Leo-III

MaRDI QIDQ4557854zbMATH OpenFDO

Authors Alexander Steen

Publication date 27 November 2018

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Recommendations

• Extensional higher-order paramodulation in Leo-III
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• The higher-order prover Leo-III
• scientific article; zbMATH DE number 5850137
• The higher-order prover \textsc{Leo}-II

Cited in

(11)

• The higher-order prover Leo-III
• Superposition with first-class booleans and inprocessing clausification
• A Knuth-Bendix-like ordering for orienting combinator equations
• A combinator-based superposition calculus for higher-order logic
• Restricted combinatory unification
• Extensional higher-order paramodulation in Leo-III
• Agent-based HOL reasoning
• scientific article; zbMATH DE number 1341621 (Why is no real title available?)
• Making higher-order superposition work
• Making higher-order superposition work
• A higher-order Vampire (short paper)

Describes a project that uses

Uses Software

• Leo-III

This page was built for publication: Extensional paramodulation for higher-order logic and its effective implementation Leo-III

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