Clausal presentation of theories in deduction modulo

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

Authors: 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

Recommendations

• Presentation of proofs in modal natural deduction
• On modal logic of deductive closure
• scientific article; zbMATH DE number 549984
• scientific article; zbMATH DE number 2086334
• Deduction theorem in congruential modal logics
• scientific article; zbMATH DE number 1523046
• scientific article; zbMATH DE number 1859172
• Clausal resolution for modal logics of confluence
• Clausal resolution for normal modal logics
• scientific article; zbMATH DE number 549980

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 (5)

• Clausal relations and {C}-clones
• Automating theories in intuitionistic logic
• Resolution is cut-free
• Title not available (Why is that?)
• MUS Extraction Using Clausal Proofs

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)