A mechanization of strong Kleene logic for partial functions

DOI10.1007/3-540-58156-1_26zbMath1433.03024OpenAlexW1491709951MaRDI QIDQ5210785

Michael Kohlhase, Manfred Kerber

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:hbz:386-kluedo-3309

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Many-valued logic (03B50) Paraconsistent logics (03B53)

Related Items

Reasoning without believing: on the mechanisation of presuppositions and partiality, Eager Equality for Rational Number Arithmetic, Modular proof systems for partial functions with Evans equality, The seven virtues of simple type theory, Classical Logic with Partial Functions, A mechanization of strong Kleene logic for partial functions, Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis

Uses Software

• IMPS

Cites Work

• A more expressive formulation of many sorted logic
• The substitutional framework for sorted deduction: Fundamental results on hybrid reasoning
• IMPS: An interactive mathematical proof system
• Computational aspects of an order-sorted logic with term declarations
• A first order logic for partial functions
• A mechanization of strong Kleene logic for partial functions
• Completeness theorems for some presupposition-free logics
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• A partial functions version of Church's simple theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item