Search

This paper introduces a logical characterization of multi-adjoint algebras with a twofold contribution. On the one hand, the study of multi-adjoint algebras, from a logical perspective, will allow us to discover both the core and new features of these algebras. On the other hand, the axiomatization of multi-adjoint algebras will be useful to take advantage of the properties of the logical connectives considered in the corresponding deductive system. The mechanism considered to carry out the mentioned axiomatization follows the one given by Petr Hajek for residuated lattices. Specifically, the paper presents the bounded poset logic (BPL) as an axiomatization of a bounded poset, since this algebraic structure is the most simple structure from which a multi-adjoint algebra is defined. In the following, the language of BPL is enriched with a family of pairs, composed of a conjunctor and an implication, and its axiomatic system is endowed with new axioms, giving rise to the multi-adjoint logic (ML). The soundness and completeness of BPL and ML are proven. Finally, a comparison between the axiomatization of the multi-adjoint logic and the one given for the BL logic is introduced.

Inquisitive first order logic "Equation missing" is an extension of first order classical logic, introducing questions and studying the logical relations between questions and quantifiers. It is not known whether "Equation missing" is recursively axiomatizable, even though an axiomatization has been found for fragments of the logic (Ciardelli, 2016). In this paper we define the $$\mathsf {ClAnt}$$ ClAnt —classical antecedent—fragment, together with an axiomatization and a proof of its strong completeness. This result extends the ones presented in the literature and introduces a new approach to study the axiomatization problem for fragments of the logic.

A logic is said to admit an equational completeness theorem when it can be interpreted into the equational consequence relative to some class of algebras. We characterize logics admitting an equational completeness theorem that are either locally tabular or have some tautology. In particular, it is shown that a protoalgebraic logic admits an equational completeness theorem precisely when it has two distinct logically equivalent formulas. While the problem of determining whether a logic admits an equational completeness theorem is shown to be decidable both for logics presented by a finite set of finite matrices and for locally tabular logics presented by a finite Hilbert calculus, it becomes undecidable for arbitrary logics presented by finite Hilbert calculi.

Some find it plausible that a sufficiently long duration of torture is worse than any duration of mild headaches. Similarly, it has been claimed that a million humans living great lives is better than any number of worm-like creatures feeling a few seconds of pleasure each. Some have related bad things to good things along the same lines. For example, one may hold that a future in which a sufficient number of beings experience a lifetime of torture is bad, regardless of what else that future contains, while minor bad things, such as slight unpleasantness, can always be counterbalanced by enough good things. Among the most common objections to such ideas are sequence arguments. But sequence arguments are usually formulated in classical logic. One might therefore wonder if they work if we instead adopt many-valued logic. I show that, in a common many-valued logical framework, the answer depends on which versions of transitivity are used as premises. We get valid sequence arguments if we grant any of several strong forms of transitivity of ‘is at least as bad as’ and a notion of completeness. Other, weaker forms of transitivity lead to invalid sequence arguments. The plausibility of the premises is largely set aside here, but I tentatively note that almost all of the forms of transitivity that lead to valid sequence arguments seem intuitively problematic. Still, a few moderately strong forms of transitivity that might be acceptable lead to valid sequence arguments, although weaker statements of the initial value claims avoid these arguments at least to some extent.

Six interesting variants of the logics BN4 and E4—which can be considered as the 4-valued logics of the relevant conditional and (relevant) entailment, respectively—were previously developed in the literature. All these systems are related to the family of relevant logics and contain Routley and Meyer's basic logic B, which is well-known to be specifically associated with the ternary relational semantics. The aim of this paper is to develop reduced general Routley-Meyer semantics for them. Strong soundness and completeness theorems are proved for each one of the logics.

Uncertain information is being taken into account in an increasing number of application fields. In the meantime, abduction has been proved a powerful tool for handling hypothetical reasoning and incomplete knowledge. Probabilistic logical models are a suitable framework to handle uncertain information, and in the last decade many probabilistic logical languages have been proposed, as well as inference and learning systems for them. In the realm of Abductive Logic Programming (ALP), a variety of proof procedures have been defined as well. In this paper, we consider a richer logic language, coping with probabilistic abduction with variables. In particular, we consider an ALP program enriched with integrity constraints `a la IFF, possibly annotated with a probability value. We first present the overall abductive language, and its semantics according to the Distribution Semantics. We then introduce a proof procedure, obtained by extending one previously presented, and prove its soundness and completeness., Paper presented at the 37th International Conference on Logic Programming (ICLP 2021), 16 pages

In this paper we analyse logic of false belief in the intuitionistic setting. This logic, studied in its classical version by Steinsvold, Fan, Gilbert and Venturi, describes the following situation: a formula $\varphi$ is not satisfied in a given world, but we still believe in it (or we think that it should be accepted). Another interpretations are also possible: e.g. that we do not accept $\varphi$ but it is imposed on us by a kind of council or advisory board. From the mathematical point of view, the idea is expressed by an adequate form of modal operator $\mathsf{W}$ which is interpreted in relational frames with neighborhoods. We discuss monotonicity of forcing, soundness, completeness and several other issues. Finally, we mention the fact that it is possible to investigate intuitionistic logics of unknown truths.

To investigate the relationship between logical reasoning and majority voting, we introduce logic with groups Lg in the style of Gentzen’s sequent calculus, where every sequent is indexed by a group of individuals. We also introduce the set-theoretical semantics of Lg, where every formula is interpreted as a certain closed set of groups whose members accept that formula. We present the cut-elimination theorem, and the soundness and semantic completeness theorems of Lg. Then, introducing an inference rule representing majority voting to Lg, we introduce logic with majority voting Lv. Formalizing the discursive paradox in judgment aggregation theory, we show that Lv is inconsistent. Based on the premise-based and conclusion-based approaches to avoid the paradox, we introduce logic with majority voting for axioms Lva, where majority voting is applied only to non-logical axioms as premises to construct a proof in Lg, and logic with majority voting for conclusions Lvc, where majority voting is applied only to the conclusion of a proof in Lg. We show that both Lva and Lvc are syntactically complete and consistent, and we construct collective judgments based on the provability in Lva and Lvc, respectively. Then, we discuss how these systems avoid the discursive paradox.

This paper investigates a first-order extension of GL called \(\textup{ML}^3\). We outline briefly the history that led to \(\textup{ML}^3\), its key properties and some of its toolbox: the \emph{conservation theorem}, its cut-free Gentzenisation, the ``formulators'' tool. Its semantic completeness (with respect to finite reverse well-founded Kripke models) is fully stated in the current paper and the proof is retold here. Applying the Solovay technique to those models the present paper establishes its main result, namely, that \(\textup{ML}^3\) is arithmetically complete. As expanded below, \(\textup{ML}^3\) is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability―"\(\Box\)" simulating the the informal classical "\(\vdash\)"―is also arithmetically complete in the Solovay sense.

We present a method for learning multi-stage tasks from demonstrations by learning the logical structure and atomic propositions of a consistent linear temporal logic (LTL) formula. The learner is given successful but potentially suboptimal demonstrations, where the demonstrator is optimizing a cost function while satisfying the LTL formula, and the cost function is uncertain to the learner. Our algorithm uses the Karush-Kuhn-Tucker (KKT) optimality conditions of the demonstrations together with a counterexample-guided falsification strategy to learn the atomic proposition parameters and logical structure of the LTL formula, respectively. We provide theoretical guarantees on the conservativeness of the recovered atomic proposition sets, as well as completeness in the search for finding an LTL formula consistent with the demonstrations. We evaluate our method on high-dimensional nonlinear systems by learning LTL formulas explaining multi-stage tasks on a simulated 7-DOF arm and a quadrotor, and show that it outperforms competing methods for learning LTL formulas from positive examples. Finally, we demonstrate that our approach can learn a real-world multi-stage tabletop manipulation task on a physical 7-DOF Kuka iiwa arm.

We propose a notion of the Kripke-style model for intersection logic. Using a game interpretation, we prove soundness and completeness of the proposed semantics. In other words, a formula is provable (a type is inhabited) if and only if it is forced in every model. As a by-product, we obtain another proof of normalization for the Barendregt–Coppo–Dezani intersection type assignment system.

A phase is an instance of derivation or “spell out’’ of a chunk or whole of a sentence construction. It is standardly assumed thatonly complementizer phrases and little v(erb) phrases are phases, and tense and verb phrases are not phases. Other categories such as determiner phrases and applicative phrases have been tested positive for phases. However, no claim is made about the status of prepositional phrases as phases. This paper investigated whether prepositional phrases in English can have the status of a phase as defined in phase theory. It was hypothesised that prepositional phrases are phases of the ‘weak’ kind. To determine the phase status of prepositional phrases, the method of standard phase diagnostics tests such as computational complexity, phonological independence, semantic independence, and case checking, and theta completeness were used. It was found out that computational complexity is not a valid test to test prepositional phrases for phasehood. While prepositional phrases bear very strong evidence to be labelled phases with respect to phonological independence, PPs fail to be phases in the case of semantic independence, and case checking and theta completeness. Given these findings, it was concluded that prepositional phrases in English are phases of the ‘weak’ kind. A sample of sentence constructions in English selected by the author and borrowed from the existing literature were used for the tests to draw conclusions. The study is expected to help better understand and analyze the cognitive processes involved in the acquisition and production of the English language specifically and any language in general. DOI : http://doi.org/10.31357/fhss/vjhss.v06i02.07

In this study, falsification-aware semantics and sequent calculi for first-order classical logic are introduced and investigated. These semantics and sequent calculi are constructed based on a falsification-aware setting for first-order Nelson constructive three-valued logic (N3). In fact, these semantics and sequent calculi are regarded as those for a classical variant of N3 (i.e., a classical variant of N3 is identical to first-order classical logic). The completeness and cut-elimination theorems for the proposed semantics and sequent calculi are proved using Schutte’s method. Similar results for the propositional case are also obtained.

The formalization of action and obligation using logic languages is a topic of increasing relevance in the field of ethics for AI. Having an expressive syntactic and semantic framework to reason about agents' decisions in moral situations allows for unequivocal representations of components of behavior that are relevant when assigning blame (or praise) of outcomes to said agents. Two very important components of behavior in this respect are belief and belief-based action. In this work we present a logic of doxastic oughts by extending epistemic deontic stit theory with beliefs. On one hand, the semantics for formulas involving belief operators is based on probability measures. On the other, the semantics for doxastic oughts relies on a notion of optimality, and the underlying choice rule is maximization of expected utility. We introduce an axiom system for the resulting logic, and we address its soundness, completeness, and decidability results. These results are significant in the line of research that intends to use proof systems of epistemic, doxastic, and deontic logics to help in the testing of ethical behavior of AI through theorem-proving and model-checking., Comment: In Proceedings TARK 2021, arXiv:2106.10886

The calculus of Natural Calculation is introduced as an extension of Natural Deduction by proper term rules. Such term rules provide the capacity of dealing directly with terms in the calculus instead of the usual reasoning based on equations, and therefore the capacity of a natural representation of informal mathematical calculations. Basic proof theoretic results are communicated, in particular completeness and soundness of the calculus; normalisation is briefly investigated. The philosophical impact on a proof theoretic account of the notion of meaning is considered.

In this article, we study logics of unknown truths and false beliefs under neighborhood semantics. We compare the relative expressivity of the two logics. It turns out that they are incomparable over various classes of neighborhood models, and the combination of the two logics are equally expressive as standard modal logic over any class of neighborhood models. We propose morphisms for each logic, which can help us explore the frame definability problem, show a general soundness and completeness result, and generalize some results in the literature. We axiomatize the two logics over various classes of neighborhood frames. Most importantly, by adopting the intersection semantics and the subset semantics in the literature, we extend the results to the case of public announcements, which gives us the desired reduction axioms and has good applications related to Moore sentences, successful formulas and self-refuting formulas. Also, we can say something about the comparative merits of the intersection semantics and the subset semantics.

Quasi-Nelson logic is a recently-introduced generalization of Nelson’s constructive logic with strong negation to a non-involutive setting. In the present paper we axiomatize the negation-implication fragment of quasi-Nelson logic (QNI-logic), which constitutes in a sense the algebraizable core of quasi-Nelson logic. We introduce a finite Hilbert-style calculus for QNI-logic, showing completeness and algebraizability with respect to the variety of QNI-algebras. Members of the latter class, also introduced and investigated in a recent paper, are precisely the negation-implication subreducts of quasi-Nelson algebras. Relying on our completeness result, we also show how the negation-implication fragments of intuitionistic logic and Nelson’s constructive logic may both be obtained as schematic extensions of QNI-logic.

This paper introduces a multi-agent dynamic epistemic logic for abstract argumentation. Its main motivation is to build a general framework for modelling the dynamics of a debate, which entails reasoning about goals, beliefs, as well as policies of communication and information update by the participants. After locating our proposal and introducing the relevant tools from abstract argumentation, we proceed to build a three-tiered logical approach. At the first level, we use the language of propositional logic to encode states of a multi-agent debate. This language allows to specify which arguments any agent is aware of, as well as their subjective justification status. We then extend our language and semantics to that of epistemic logic, in order to model individuals’ beliefs about the state of the debate, which includes uncertainty about the information available to others. As a third step, we introduce a framework of dynamic epistemic logic and its semantics, which is essentially based on so-called event models with factual change. We provide completeness results for a number of systems and show how existing formalisms for argumentation dynamics and unquantified uncertainty can be reduced to their semantics. The resulting framework allows reasoning about subtle epistemic and argumentative updates—such as the effects of different levels of trust in a source—and more in general about the epistemic dimensions of strategic communication.

In this paper, we give an alternative semantics to the non-normal logic of knowing how proposed by Fervari et al. (Proc IJCAI 2017:1031–1038, 2017), based on a class of Kripke neighborhood models with both the epistemic relations and neighborhood structures. This alternative semantics is inspired by the same quantifier alternation pattern of $$\exists \forall $$ in the semantics of the know-how modality and the (monotonic) neighborhood semantics for the standard modality. We show that this new semantics is equivalent to the original Kripke semantics in terms of the validities. A key result is a representation theorem showing that the more abstract Kripke neighborhood models can be represented by the concrete Kripke models with action transitions modulo the valid formulas. We prove the completeness of the logic for the neighborhood semantics. The neighborhood semantics can be adapted to other variants of logics of knowing how. It provides us a powerful technical tool to study these logics while preserving the basic semantic intuition.

Action logic is the algebraic logic (inequational theory) of residuated Kleene lattices. One of the operations of this logic is the Kleene star, which is axiomatized by an induction scheme. For a stronger system that uses an -rule instead (infinitary action logic), Buszkowski and Palka (2007) proved -completeness (thus, undecidability). Decidability of action logic itself was an open question, raised by Kozen in 1994. In this article, we show that it is undecidable, more precisely, -complete. We also prove the same undecidability results for all recursively enumerable logics between action logic and infinitary action logic, for fragments of these logics with only one of the two lattice (additive) connectives, and for action logic extended with the law of distributivity.

In this study, we introduce Gentzen-type sequent calculi BDm and BDi for a modal extension and an intuitionistic modification, respectively, of De and Omori’s extended Belnap–Dunn logic BD+ with classical negation. We prove theorems for syntactically and semantically embedding BDm and BDi into Gentzen-type sequent calculi S4 and LJ for normal modal logic and intuitionistic logic, respectively. The cut-elimination, decidability, and completeness theorems for BDm and BDi are obtained using these embedding theorems. Moreover, we prove the Glivenko theorem for embedding BD+ into BDi and the McKinsey–Tarski theorem for embedding BDi into BDm.

UNITY is a model for concurrent specifications with a complete logic for proving progress properties of the form “ P leads to Q ”. UNITY is generalized to U-specifications by giving more freedom to specify the steps that are to be taken infinitely often. In particular, these steps can correspond to non-total relations. The generalization keeps the logic sound and complete. The paper exploits the generalization in two ways. Firstly, the logic remains sound when the specification is extended with hypotheses of the form “ F leads to G ”. As the paper shows, this can make the logic incomplete. The generalization is used to show that the logic remains complete, if the added hypotheses “ F leads to G ” satisfy “ F unless G ”. The main result extends the applicability and completeness of UNITY logic to proofs that a given concurrent program satisfies any given formula of LTL, linear temporal logic, without the next-operator which is omitted because it is sensitive to stuttering. For this purpose, the program, written as a UNITY program, is extended with a number of boolean variables. The proof method relies on implementing the LTL formula, i.e., restricting the specification in such a way that only those runs remain that satisfy the formula. This result is a variation of the classical construction of a Büchi automatonfor a given LTL formula that accepts precisely those runs that satisfy the formula.

Fil: Castano, Diego Nicolas. Consejo Nacional de Investigaciones Cientificas y Tecnicas. Centro Cientifico Tecnologico Conicet - Bahia Blanca. Instituto de Matematica Bahia Blanca. Universidad Nacional del Sur. Departamento de Matematica. Instituto de Matematica Bahia Blanca; Argentina

Positive monotone modal logic is the negation- and implication-free fragment of monotone modal logic, i.e., the fragment with connectives and . We axiomatise positive monotone modal logic, give monotone neighbourhood semantics based on posets, and prove soundness and completeness. The latter follows from the main result of this paper: a (categorical) duality between so-called $$M^+$$ -spaces (poset-based monotone neighbourhood frames with extra structure) and the algebraic semantics of positive monotone modal logic. The main technical tool is the use of coalgebra.

In Part I of this paper, we identified and compared various schemes for trivalent truth conditions for indicative conditionals, most notably the proposals by de Finetti (1936) and Reichenbach (1935, 1944) on the one hand, and by Cooper (Inquiry, 11, 295–320, 1968) and Cantwell (Notre Dame Journal of Formal Logic, 49, 245–260, 2008) on the other. Here we provide the proof theory for the resulting logics and , using tableau calculi and sequent calculi, and proving soundness and completeness results. Then we turn to the algebraic semantics, where both logics have substantive limitations: allows for algebraic completeness, but not for the construction of a canonical model, while fails the construction of a Lindenbaum-Tarski algebra. With these results in mind, we draw up the balance and sketch future research projects.

The non-alethic systems N1 of da Costa and A of Grana are both paraconsistent and paracomplete. Based on them, a multi-agent doxastic logic NADK can be obtained by logical expansion. The soundness and completeness of NADK are proved and its special theorems are also presented. In this logic, the belief version of the laws of contradiction and excluded middle, as well as the principle of explosion are all invalid. Therefore, it may provide a reliable logical basis for any theory which has paraconsistent or paracomplete epistemic conflicts, such as true contradictions, true contrarieties, and belief paradoxes. We also explain in detail how a non-alethic doxastic logic provides a reliable logical basis for tolerating these three types of epistemic conflicts. The present paper is the deepening and development of system N1 and A.

This paper combines propositional dynamic logic ( $${\textsf {PDL}}$$ ) with propositional inquisitive logic ( $$\textsf {InqB}$$ ). The result of this combination is a logical system $$\textsf {InqPDL}$$ that conservatively extends both $${\textsf {PDL}}$$ and $$\textsf {InqB}$$ , and, moreover, allows for an interaction of the question-forming operator from $$\textsf {InqB}$$ with the structured modalities from $${\textsf {PDL}}$$ . We study this system from a semantic as well as a syntactic point of view. These two perspectives are linked via a completeness proof, which also shows that $$\textsf {InqPDL}$$ is decidable.

This paper and its sequel “look under the hood” of the usual sorts of proof-theoretic systems for certain well-known intuitionistic and classical propositional modal logics. Section 1 is preliminary. Of most importance: a marked formula will be the result of prefixing a formula in a propositional modal language with a step-marker, for this paper either 0 or 1. Think of 1 as indicating the taking of “one step away from 0.” Deductions will be constructed using marked formulas. Section 2 presents the model-theoretic concepts, based on those in [7], that guide the rest of this paper. Section 3 presents Natural Deduction systems IK and CK, formalizations of intuitionistic and classical one-step versions of K. In these systems, occurrences of step-markers allow deductions to display deductive structure that is covered over in familiar “no step” proof-theoretic systems for such logics. $\square $ and ♢ are governed by Introduction and Elimination rules; the familiar K rule and Necessitation are derived (i.e. admissible) rules. CK will be the result of adding the 0-version of the Rule of Excluded Middle to the rules which generate IK. Note: IK is the result of merely dropping that rule from those generating CK, without addition of further rules or axioms (as was needed in [7]). These proof-theoretic systems yield intuitionistic and classical consequence relations by the obvious definition. Section 4 provides some examples of what can be deduced in IK. Section 5 defines some proof-theoretic concepts that are used in Section 6 to prove the soundness of the consequence relation for IK (relative to the class of models defined in Section 2.) Section 7 proves its completeness (relative to that class). Section 8 extends these results to the consequence relation for CK. (Looking ahead: Part 2 will investigate one-step proof-theoretic systems formalizing intuitionistic and classical one-step versions of some familiar logics stronger than K.)

We translate the three-valued quantum logic into modal logic, and prove 3-equivalence between the valuation of the three-valued logic and a kind of Kripke model in regard to this translation. To prove 3-equivalence, we introduce an observable-dependent logic, which is a fragment of the many-valued quantum logic. Compared to the Birkhoff and von Neumann’s quantum logic, some notions about observables, the completeness relation for example, in quantum mechanics can be utilized if the observable-dependent logic is employed.

This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting's nested calculi naturally arise from their corresponding labelled calculi--for each of the aforementioned logics--via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic's semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic's semantics., arXiv admin note: text overlap with arXiv:1910.06576

Chemistry is a subject that is closely related to learning that requires students to be active in problem solving. Because of this, a worksheet development is needed to support chemistry learning activities. This research aims to develop a Student Based Worksheet (LKPD) based on Problem Based Learning (PBL) hydrolysis material to improve mathematical logical intelligence. The quality of LKPD is measured by the criteria of validity, effectiveness, and practicality in the learning process. The development model used in this research is a 3D model (define, design and develop). Data analysis techniques using qualitative and quantitative tests. The product development validation was carried out by the validator of media experts and material experts, while the trial was conducted by 36 students of class XI IPA 5. The results of the validator analysis stated that the quality of learning material was included in the excellent category with a percentage of 93.77% of the material experts and 94.46% of media experts. The effectiveness of LKPD indicated an increase in mathematical logical intelligence of students with the achievement of N-gain of 0.56 in the medium category and classical completeness of 86.11%. Student responses to the practicality of using LKPD showed results of 77.78% which included in the very good category and 22.22% included in the good category. Based on the results obtained, it can be concluded that LKPD fulfills valid, effective, practical criteria, and can improve mathematical logical intelligence.

This article is devoted to the analysis and formulation of requirements for judicial documents. The relevance of the stated topic is explained by the need to improve the communication process and improve the efficiency of justice. The most developed are the issues of requirements for judicial acts. At the same time, the requirements for other judicial documents - petitions, statements, written evidence are important. The most important are the requirements of legality, validity, motivation. However, we must not forget such requirements as completeness, consistency, literacy. As part of the general characteristics of judicial documents, attention was paid to the requirement of fairness and expediency. Close attention is paid to the language and style of court documents. The requirements for the form and content of court documents are formulated. The author comes to the conclusion that it is necessary to legislate the requirements for some varieties of judicial documents, just as the requirements for judicial acts are fixed.

This article uses Kafka's short story 'Before the Law' to offer a reading of Al Ewing's The Immortal Hulk. This is in turn used to explore our desire to encounter the Law understood as a form of completeness. The article differentiates between 'the Law' as completeness or limitlessness and 'the law' understood as limitation. The article also examines this desire to experience completeness or limitlessness in the work of George Bataille who argued such an experience was the path to sovereignty. In response it also considers Francois Flahault's critique of Bataille who argued Bataille failed to understand limitlessness is split between a 'good infinite' and a 'bad infinite', and that it is only the latter that can ultimately satisfy us. The article then proposes The Hulk, especially as presented in Al Ewing's The Immortal Hulk, is a study in where our desire for limitlessness can take us. Ultimately it proposes we turn ourselves away from the Law and towards the law that preserves and protects our incompleteness.

Розглядаються роль й місце композиції у видавничій комунікації, основні форми структуризаціїї авторських оригіналів. Аналізуються особливості архітектоніки ви дання залежно від функціонального призначення та чи тацької адреси книги. Викладаються принципові засади організації фактичного матеріалу на рівні композиційної структуризації видавничих оригінал-макетів. Пропонується формула визначення інформаційної місткості тексту як основи оцінки релевантності контенту, його відповідності редакторським вимогам щодо якості фактичного матеріалу в частині його доцільності та повноти. Розкриваються фахова сутність композиції видання та її відмінності від композиції авторських оригіналів. Подано типологічні характеристики апарату книги як важливої складової композиції та видавничої комунікації. The role and place of composition in publishing communi cation, the main forms of structuring of author’s originals are considered. Features of the publication’s architectonics depending on the functional purpose and the reader’s ad dress of the book are analyzed. The basic principles of orga nization of factual material at the level of compositional struc turing of publishing original layouts are stated. The formula of definition of information capacity of the text as a basis for estimation of content’s relevance, its conformity to edi torial requirements concerning quality of actual material in a part of its expediency and completeness is offered. The professional essence of the composition of the pub lication and its differences from the composition of the author’s originals are revealed. The typological charac teristics of the book apparatus as an important compo nent of composition and publishing communication are given.

Propositional logic, with the aid of SAT solvers, has become capable of solving a range of important and complicated problems. Expanding this range, to contain additional varieties of problems, is subject to the complexity resulting from encoding counting constraints in conjunctive normal form (CNF). Due to the limitation of the expressive power of propositional logic, generally, such an encoding increases the numbers of variables and clauses excessively. This work eliminates the indicated drawback by interpolating constraint symbols and the set of natural numbers $${\mathbb {N}}$$ into the alphabet of propositional logic and adjusting the underlying language accordingly. In the extended logic counting constraints are naturally formulated, while many important aspects, such as Boolean nature and the soundness and completeness theorems, are kept preserved.

Theorem proving is one of the most widely used approaches to the verification of computer systems, and its theoretical basis is generally a proof system for formal derivation of logic formulas. In this paper, we propose a sound and complete proof system for Propositional Projection Temporal Logic (PPTL) with indexed expressions, which is a unified temporal logic that subsumes the well used Linear Temporal Logic (LTL). First, the syntax, semantics and logic laws of PPTL that allows indexed expressions are introduced, and the representation of LTL constructs by PPTL formulas is illustrated. Then, the proof system for the logic is presented which consists of axioms and inference rules for the derivation of both basic constructs and indexed expressions. To show the capability of the proof system, several examples of formal proofs are provided. Finally, the soundness and completeness of the proof system are demonstrated.

Thom Fr\"uhwirth presented a short, elegant and efficient Prolog program for the n queens problem. However the program may be seen as rather tricky and one may not be convinced about its correctness. This paper explains the program in a declarative way, and provides proofs of its correctness and completeness. The specification and the proofs are declarative, i.e. they abstract from any operational semantics. The specification is approximate, it is unnecessary to describe the program's semantics exactly. Despite the program works on non-ground terms, this work employs the standard semantics, based on logical consequence and Herbrand interpretations. Another purpose of the paper is to present an example of precise declarative reasoning about the semantics of a logic program. Under consideration in Theory and Practice of Logic Programming (TPLP)., Comment: Under consideration in Theory and Practice of Logic Programming (TPLP). 13 pages, 1 figure. A re-worked version of arXiv:1909.07479

C. I. Lewis’ systems were the first axiomatisations of modal logics. However some of those systems are non-normal modal logics, since they do not admit a full rule of necessitation, but only a restricted version thereof. We provide G3-style labelled sequent calculi for Lewis’ non-normal propositional systems. The calculi enjoy good structural properties, namely admissibility of structural rules and admissibility of cut. Furthermore they allow for straightforward proofs of admissibility of the restricted versions of the necessitation rule. We establish completeness of the calculi and we discuss also related systems.

The authors present a theoretical proposal for the organization of mathematical contents, more precisely to curricula development formalization and formal verification, inspired by knowledge engineering techniques. The situation addressed is the following: the starting point is a mathematical “official curriculum” (or part of it), not necessarily completely detailed. In our proposal, a group of experts would have to first build a detailed formulation of this curriculum (including the “prerequisite” relation between contents), which we will denominate “preprocessed official curriculum.” We detail how any “official curriculum development” could then be rigorously formalized and formally verified in a way inspired by rule-based expert system formal verification. We have defined the following terms: “contents soundness,” “contents completeness,” “relation soundness,” “relation completeness,” and “absence of cycles.” We believe that this is a completely new formalization within mathematics teaching theory that, once computer is implemented, would be very helpful. That would be the case, for instance, in countries where government sets the “official curricula” for Primary and Secondary Education and textbook contents have to be manually checked and approved by academic authorities: evaluators would “only” have to extract the textbook contents and set the “prerequisite” relation among them and let the computer do the rest.

In this paper a generalisation of the inference rules of the join dependencies that are used in the design of database schemas that meets the requirements of the fifth normal form is considered. In the previous works devoted to this problem, attempts to construct systems of the axioms of such dependencies based on inference rules are made. However, while the justification for the consistency (soundness) of the obtained axioms does not cause difficulties, the proof of completeness in general has not been satisfactorily resolved. First of all, this is due to the limitations of the inference rules themselves. This work focuses on two original axiom systems presented in the works of Sciore and Malvestuto. For the inclusion dependencies a system of rules that generalises existing systems and has fewer restrictions has been obtained. The paper presents a proof of the derivability of known systems of axioms from the presented inference rules. In addition, evidence of the consistency (soundness) of these rules is provided. The question of the completeness of the formal system based on the presented rules did not find a positive solution. In conclusion, the theoretical and practical significance of the inference rules for the join dependencies is noted.

An approach for formal verification of UML 2.0 using mapping OWL-DL in UML 2.0 is proposed. As a result, an original approach for mapping OWL-DL to UML 2.0 through description logic has been proposed. The completeness of the mapping of UML-OWL through stereotypes and labeled UML 2.0 values at the level of M0, M1 of the MOF metamodel is provided. A model of the information object (IO) for the semantic electronic library, which is described by using the UML language, is proposed. The proposed IO model was also verified by mapping it into OWL and then validating the constructed ontology by using risoners. Problems in programming 2020; 2-3: 31-38

Supporting inductive reasoning is an essential component is any framework of use in computer science. To do so, the logical framework must extend that of first-order logic. Transitive closure logic is a known extension of first-order logic that is particularly straightforward to automate. While other extensions of first-order logic with inductive definitions are a priori parametrized by a set of inductive definitions, the addition of a single transitive closure operator has the advantage of uniformly capturing all finitary inductive definitions. To further improve the reasoning techniques for transitive closure logic, we here present an infinitary proof system for it, which is an infinite descent –style counterpart to the existing (explicit induction) proof system for the logic. We show that the infinitary system is complete for the standard semantics and subsumes the explicit system. Moreover, the uniformity of the transitive closure operator allows semantically meaningful complete restrictions to be defined using simple syntactic criteria. Consequently, the restriction to regular infinitary (i.e., cyclic ) proofs provides the basis for an effective system for automating inductive reasoning.

We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories. We show the correctness of our definitions by proving conservative extension theorems, which state that a sequent/judgment is provable in the original system if and only if it is provable in matching logic, in the corresponding theory. Our matching logic definition of binders also yields models to all binders, which are deductively complete with respect to formal reasoning in the original systems. For lambda-calculus, we further show that the yielded models are representationally complete, a desired property that is not enjoyed by many existing lambda-calculus semantics. This work is part of a larger effort to develop a logical foundation for the programming language semantics framework K (http://kframework.org).

In this paper, $$\alpha $$ -paramodulation and $$\alpha $$ -GH paramodulation methods are proposed for handling logical formulae with equality in a lattice-valued logic $$L_nF(X)$$ , which has unique ability for representing and reasoning uncertain information from a logical point of view. As an extension of the work of He et al. (in: 2015 10th international conference on intelligent systems and knowledge engineering (ISKE), pp 18–20. IEEE, 2015; Uncertainty modelling in knowledge engineering and decision making: proceedings of the 12th international FLINS conference, pp 477–482. World Scientific, 2016), a new form of $$\alpha $$ -equality axioms set is proposed. The equivalence between $$\alpha $$ -equality axioms set and $$E_{\alpha }$$ -interpretation in $$L_nF(X)$$ with an appropriate level is also established, which may provide a key foundation for equality reasoning in lattice-valued logic. Based on its equivalence, $$E_{\alpha }$$ -unsatisfiability equivalent transformation is given. Furthermore, $$\alpha $$ -paramodulation and its restricted method (i.e., $$\alpha $$ -GH paramodulation) are given. The soundness and completeness of the proposed methods are also examined.

Cirquent calculus is a novel proof theory permitting component-sharing between logical expressions. Using it, the predecessor article ‘Elementary-base cirquent calculus I: Parallel and choice connectives’ built the sound and complete axiomatization $\textbf{CL16}$ of a propositional fragment of computability logic. The atoms of the language of $\textbf{CL16}$ represent elementary, i.e. moveless, games and the logical vocabulary consists of negation, parallel connectives and choice connectives. The present paper constructs the first-order version $\textbf{CL17}$ of $\textbf{CL16}$, also enjoying soundness and completeness. The language of $\textbf{CL17}$ augments that of $\textbf{CL16}$ by including choice quantifiers. Unlike classical predicate calculus, $\textbf{CL17}$ turns out to be decidable.

INTRODUCTION Nontechnical skills (NTS) have been acknowledged to be important for medical students and can be linked to improved clinical performance. However, existing tools to evaluate these within a simulated setting address only a limited number of NTS. The Medical Students' Nontechnical Skills (Medi-StuNTS) behavioral marker system (BMS) outlines 5 categories of NTS for medical students. This study aimed to seek evidence for completeness and content validity to refine the BMS and to ascertain which NTS are essential for medical students. METHODS We asked 128 workshop participants if they felt there were any missing or irrelevant items in Medi-StuNTS system. A subject matter expert panel (n = 10) rated how essential they considered each item in the BMS. An Item-Content Validity Index was calculated for each skill element and the Scale-Content Validity Index was calculated as a measure of content validity of the full system. RESULTS Of the workshop participants, 78.9% felt that there were no missing items and 93% felt that there were no irrelevant items. Potentially missing items highlighted were as follows: "working in a hierarchy," "leadership," "awareness of the emotional state of other team members," and "nonverbal communication." Fourteen of 16 skill elements achieved the recommended level for content validity (Item-Content Validity Index ≥ 0.78), and the Scale-Content Validity Index was higher than the acceptable level (≥0.8). CONCLUSIONS Evidence for completeness and content validity of Medi-StuNTS has been demonstrated. There is a far wider range of NTS that seem to be essential for medical students than those assessed by tools developed before Medi-StuNTS. Medi-StuNTS provides comprehensive cover of the essential NTS required by medical students, with specific reference to the skill categories "self-awareness" and "escalating care," which do not feature in other tools for assessing NTS in this group.

To specify and verify the concurrent and reactive systems with the theorem proving approach, a complete axiomatization is formalized for first order projection temporal logic (PTL) with both finite and infinite time. To this end, PTL is restricted to a finite domain, and the syntax, semantics as well as the axiomatization of PTL are presented. Further, the techniques of labeled normal form and labeled normal form graph of PTL formulas are introduced respectively, with which a decision procedure for quantifier free PTL (QFPTL) formulas is given. Moreover, a generalized labeled normal form graph is defined and employed to transform a quantified PTL formula into its equivalent QFPTL formula. Finally, a decision procedure for PTL is formalized and the completeness of the axiomatic system is proved based on the decidability of PTL formulas.

We present the logic $${\mathsf {LCB}}$$ LCB which is expressed in a propositional language constantly enriched by new atomic expressions. Our formal framework is the propositional doxastic logic $${\mathsf {KD45}}$$ KD 45 with the belief operator $${\mathcal {B}}$$ B , extended by the $${\mathcal {C}}$$ C operator, to be read it changes that ... . We describe the changing beliefs of an agent who uses progressively expanding language. The approach presented here allows us to weaken pragmatic objections to the so-called principle of negative retrospection accepted in $${\mathsf {KD45}}$$ KD 45 and the problem of logical omniscience. In what follows, we present the expanding propositional language used in our formalism, interpreted using an epistemic version of Kripke semantics. Next, we give a syntactic characterization of logic $${\mathsf {LCB}}$$ LCB and prove the soundness and completeness of $${\mathsf {LCB}}$$ LCB in respect to our semantics. Finally, we compare the idea of expanding language with the notion of agent awareness and we relate our formalism to two epistemic temporal logics.

This paper proposes a generalization of the Kripke semantics of intuitionistic logicIL appropriate forintuitionistic Łukasiewicz logicIŁL —a logic in the intersection betweenIL and (classical) Łukasiewicz logic. This generalised Kripke semantics is based on theposet sumconstruction, used in Bova and Montagna (Theoret Comput Sci 410(12):1143–1158, 2009). to show the decidability (and PSPACE completeness) of the quasiequational theory of commutative, integral and bounded GBL algebras. The main idea is that$$w \Vdash \psi $$w⊩ψ—which forILis a relation between worldswand formulas$$\psi $$ψ, and can be seen as a function taking values in the booleans$$(w \Vdash \psi ) \in {{\mathbb {B}}}$$(w⊩ψ)∈B—becomes a function taking values in the unit interval$$(w \Vdash \psi ) \in [0,1]$$(w⊩ψ)∈[0,1]. An appropriate monotonicity restriction (which we callsloping functions) needs to be put on such functions in order to ensure soundness and completeness of the semantics.

Two intuitionistic paradefinite logics N4C and N4C+ are introduced as Gentzen-type sequent calculi. These logics are regarded as a combination of Nelson’s paraconsistent four-valued logic N4 and Wansing’s basic constructive connexive logic C. The proposed logics are also regarded as intuitionistic variants of Arieli, Avron, and Zamansky’s ideal paraconistent four-valued logic 4CC. The logic N4C has no quasi-explosion axiom that represents a relationship between conflation and paraconsistent negation, but the logic N4C+ has this axiom. The Kripke-completeness and cut-elimination theorems for N4C and N4C+ are proved.