Pure first-order quasiary logics with equality predicates
Logics of quasiary predicates are program-oriented logics which aim to reflect such program properties as partiality, non-determinism, and non-fixed arity. In the paper, program-oriented logical formalisms – pure first-order logics of partial deterministic and non-deterministic predicates – are stud...
Saved in:
| Date: | 2018 |
|---|---|
| Main Authors: | , |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
PROBLEMS IN PROGRAMMING
2018
|
| Subjects: | |
| Online Access: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/316 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Problems in programming |
| Download file: |  |
Institution
Problems in programming| Summary: | Logics of quasiary predicates are program-oriented logics which aim to reflect such program properties as partiality, non-determinism, and non-fixed arity. In the paper, program-oriented logical formalisms – pure first-order logics of partial deterministic and non-deterministic predicates – are studied. The main attention is paid to logics with special equality relations. Logics with weak equality and strong equality are defined, their properties are investigated. Languages of such logics and their interpetations are described. The following classes of interpretations (semantics) are identified: partial deterministic, non-deterministic, total deterministic, and total non-deterministic interpetations. Semantic properties of the proposed logics are investigated. Special attention is paid to consequence relations for sets of formulas. Based on the properties of these relations a number of calculi of sequent type is proposed. Basic rules of these calculi and corresponding closedness conditions are formulated; the procedure of sequent tree construction is described. For the proposed calculi correctness and completeness theorems are proved. The proof of completeness is based on the construction of countermodel for an unclosed path in the sequent tree.Problems in programming 2017; 2: 03-23 |
|---|