2023/05/25 by Gilles Dowek, Dowek, Gilles · 1 citation
Computer Science · Psychology · #Advanced Algebra and Logic #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Philosophy and Theoretical Science
paper · pdf · doi:10.48550/arxiv.2305.15780
openalex publication_date 2023/05/25 · openalex created_date 2023/05/27 · openalex updated_date 2026/07/28
Deduction modulo is a way to express a theory using computation rules instead of axioms. We present in this paper an extension of deduction modulo, called Polarized deduction modulo, where some rules can only be used at positive occurrences, while others can only be used at negative ones. We show that all theories in propositional calculus can be expressed in this framework and that cuts can always be eliminated with such theories.