A completeness proof for a regular predicate logic with undefined truth value
From MaRDI portal
Publication:6100982
Abstract: We provide a sound and complete proof system for an extension of Kleene's ternary logic to predicates. The concept of theory is extended with, for each function symbol, a formula that specifies when the function is defined. The notion of "is defined" is extended to terms and formulas via a straightforward recursive algorithm. The "is defined" formulas are constructed so that they themselves are always defined. The completeness proof relies on the Henkin construction. For each formula, precisely one of the formula, its negation, and the negation of its "is defined" formula is true on the constructed model. Many other ternary logics in the literature can be reduced to ours. Partial functions are ubiquitous in computer science and even in (in)equation solving at schools. Our work was motivated by an attempt to explain, precisely in terms of logic, typical informal methods of reasoning in such applications.
Recommendations
- scientific article; zbMATH DE number 4035828
- scientific article; zbMATH DE number 3931008
- An intuitionistic completeness theorem for classical predicate logic
- A completeness theorem for continuous predicate modal logic
- Some Completeness Results for Propositional Conditional Logics
- The completeness of a predicate-functor logic
- A logic for propositions with indefinite truth values
- Completeness theory for propositional logics
- scientific article; zbMATH DE number 2196603
- A proof of the standard completeness for the involutive uninorm logic
Cites work
- scientific article; zbMATH DE number 1001667 (Why is no real title available?)
- scientific article; zbMATH DE number 42431 (Why is no real title available?)
- scientific article; zbMATH DE number 49488 (Why is no real title available?)
- scientific article; zbMATH DE number 610968 (Why is no real title available?)
- scientific article; zbMATH DE number 1867305 (Why is no real title available?)
- scientific article; zbMATH DE number 2217307 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- A first order logic for partial functions
- A fully logical inductive logic
- A logic covering undefinedness in program proofs
- A more unified approach to free logics
- A practical approach to partial functions in CVC Lite
- A set theory with support for partial functions
- A system of logic for partial functions under existence-dependent kleene equality
- A typed logic of partial functions reconstructed classically
- Adapting Calculational Logic to the Undefined
- Computer science today. Recent trends and developments
- Efficient Well-Definedness Checking
- Natural deduction for three-valued regular logics
- On all strong Kleene generalizations of classical logic
- Problems in between words and abelian words: \(k\)-abelian avoidability
- Strict Fregean free logic
- The completeness of the first-order functional calculus
- Theorem proving for classical logic with partial functions by reduction to Kleene logic
Cited in
(3)
This page was built for publication: A completeness proof for a regular predicate logic with undefined truth value
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6100982)
