On the practical value of Herbrand disjunctions

DOI10.12775/LLP.2000.009MaRDI QIDQ3149221zbMATH OpenFDO

Authors Uwe Petermann

Publication date 25 February 2003

Published in Logic and Logical Philosophy (Search for Journal in Brave)

zbMATH Keywords

automatic theorem provingnormal form transformationsHerbrand disjunctionsheterogeneous theoriesopen theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Describing proofs by short tautologies
• scientific article; zbMATH DE number 4204310
• Extracting Herbrand disjunctions by functional interpretation
• Herbrand's Theorem for Nonstandard Inference Operations
• Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem

Cited in

(4)

• On two classical results in the first order logic
• scientific article; zbMATH DE number 3557752 (Why is no real title available?)
• scientific article; zbMATH DE number 1841838 (Why is no real title available?)
• On the complexity of finding falsifying assignments for Herbrand disjunctions

This page was built for publication: On the practical value of Herbrand disjunctions

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