Clausal presentation of theories in deduction modulo

DOI10.1007/S11390-013-1399-0zbMath1296.03009OpenAlexW2058197979MaRDI QIDQ744331

Jian-Hua Gao

Publication date: 7 October 2014

Published in: Journal of Computer Science and Technology (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00614251/file/Gao.pdf

zbMATH Keywords

resolutioncut-free proofclausededuction modulo

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Proofs and algorithms. An introduction to logic and computability
• Resolution is cut-free
• Theorem proving modulo
• Regaining cut admissibility in deduction modulo using abstract completion
• Polarized Resolution Modulo
• Experimenting with Deduction Modulo
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: Clausal presentation of theories in deduction modulo