On the practical value of Herbrand disjunctions

DOI10.12775/LLP.2000.009zbMATH Open1005.03014MaRDI QIDQ3149221FDOQ3149221

Authors: Uwe Petermann 

Publication date: 25 February 2003

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

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

zbMATH Keywords

automatic theorem provingnormal form transformationsHerbrand disjunctionsheterogeneous theoriesopen theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (4)

• Title not available (Why is that?)
• Title not available (Why is that?)
• On the complexity of finding falsifying assignments for Herbrand disjunctions
• On two classical results in the first order logic

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)