Extensional higher-order paramodulation and RUE-resolution

DOI10.1007/3-540-48660-7_39MaRDI QIDQ4263170zbMATH OpenFDO

Authors Christoph Benzmüller

Publication date 29 May 2000

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

Full work available at URL https://doi.org/10.1007/3-540-48660-7_39

zbMATH Keywords

automated theorem provingHenkin modelparamodulationresolution

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

Several interesting results obtained by the author in his Ph.D. thesis are presented. More precisely, two approaches to primitive equality treatment in higher-order automated theorem proving are presented: a calculus adapting first-order paramodulation and a calculus adapting first-order RUE-Resolution to classical type theory. Both approaches are compared by examples. For the entire collection see [Zbl 0917.00015].

Recommendations

• Extensional higher-order resolution
• Extensional higher-order paramodulation in Leo-III
• Extensional paramodulation for higher-order logic and its effective implementation Leo-III
• Paramodulation with non-monotonic orderings and simplification
• scientific article; zbMATH DE number 1763411
• Paramodulation with Well-founded Orderings
• scientific article; zbMATH DE number 2043525
• On a generalization of extended resolution
• Automata, Languages and Programming
• Higher-order semantics and extensionality

Cited in

(14)

• Comparing approaches to resolution based higher-order theorem proving
• Superposition with first-class booleans and inprocessing clausification
• Cut-elimination for quantified conditional logic
• Extensional higher-order paramodulation in Leo-III
• The higher-order prover \textsc{Leo}-II
• scientific article; zbMATH DE number 35423 (Why is no real title available?)
• Extensional higher-order resolution
• scientific article; zbMATH DE number 1552534 (Why is no real title available?)
• Automated Deduction – CADE-20
• Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
• Superposition with lambdas
• Superposition with lambdas
• Combining and automating classical and non-classical logics in classical higher-order logics
• Types, Tableaus and Gödel’s God in Isabelle/HOL

Describes a project that uses

Uses Software

• Leo

This page was built for publication: Extensional higher-order paramodulation and RUE-resolution

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