A strong version of Herbrand's theorem for introvert sentences

DOI10.2307/2586849zbMath0908.03007OpenAlexW2099317626MaRDI QIDQ4212920

Tore Langholm

Publication date: 2 March 1999

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2586849

zbMATH Keywords

Herbrand theorem\(\mathcal R\)-non-expanding clauseground instanceintrovert clause

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Basic properties of first-order languages and structures (03C07)

Related Items (1)

Some techniques for proving termination of the hyperresolution calculus

Cites Work

• Solvable cases of the decision problem
• An algorithm for reasoning about equality
• Automatic recognition of tractability in inference relations

This page was built for publication: A strong version of Herbrand's theorem for introvert sentences