Towards automated reasoning in Herbrand structures

DOI10.1093/logcom/exz011zbMath1444.03158OpenAlexW2946845296MaRDI QIDQ5213391

Liron Cohen, Reuben N. S. Rowe, Yoni Zohar

Publication date: 3 February 2020

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://kar.kent.ac.uk/73527/1/herbrand-jlc.pdf

zbMATH Keywords

sequent calculinon-classical logicsinduction principlescyclic proofsnon-well-founded proofs\(\omega\)-ruleHerbrand logic

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

Non-well-founded deduction for induction and coinduction, Integrating induction and coinduction via closure operators and proof cycles