Canonical Inference for Implicational Systems

Completion is a general paradigm for applying inferences to generate a canonical presentation of a logical theory, or to semi-decide the validity of theorems, or to answer queries. We investigate what canonicity means for implicational systems that are axiomatizations of Moore families

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Maria Paola Bonacina, Nachum Dershowitz
• Keywords: CADE 2008, Canonical Systems, Implicational Systems, Logical Reasoning, Propositional Horn Theories