Theorem proving for classical logic with partial functions by reduction to Kleene logic

DOI10.1093/LOGCOM/EXU071zbMath1444.03014OpenAlexW1971227473MaRDI QIDQ2987064

Hans de Nivelle

Publication date: 17 May 2017

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/6e9e53b73cdfbfdcc88e3cdd889433de6c5ecfab

zbMATH Keywords

sequent calculuspartial functionsthree-valued logicautomated theorem provingfinite model search

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

A completeness proof for a regular predicate logic with undefined truth value ⋮ Subsumption Algorithms for Three-Valued Geometric Resolution

Uses Software

• Darwin
• E-Darvin
• Chaff
• CVC Lite
• ModGen
• Geo 2007F

This page was built for publication: Theorem proving for classical logic with partial functions by reduction to Kleene logic