Clausal presentation of theories in deduction modulo

DOI10.1007/S11390-013-1399-0zbMATH Open1296.03009OpenAlexW2058197979MaRDI QIDQ744331FDOQ744331

Jianhua 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

resolutionclausededuction modulocut-free proof

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (3)

• Clausal relations and {C}-clones
• Title not available (Why is that?)
• MUS Extraction Using Clausal Proofs

   Recommendations

• Presentation of proofs in modal natural deduction 👍 👎
• On modal logic of deductive closure 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Deduction theorem in congruential modal logics 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Clausal Resolution for Modal Logics of Confluence 👍 👎
• Clausal resolution for normal modal logics 👍 👎
• Title not available (Why is that?) 👍 👎

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

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