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

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

This page was built for publication: A mechanization of strong Kleene logic for partial functions