Museum of Outstanding Figures in Ukrainian Culture

This paper deals with a famous problem of epistemic logic – logical omniscience. Logical omniscience occurs in the logical systems where the axiomatics is complete and consequently an agent using inference rules knows everything about the system. Logical omniscience is a major problem due to complexity problems and the inability for adequate human reasoning modeling. It is studied both informal logic and philosophy of psychology (bounded rationality). It is important for bounded rationality because it reflects the problem of formal characterization of purely psychological mechanisms. Paper proposes to solve it using the ideas from the philosophical bounded rationality and intuitionistic logic. Special regions of deductible formulas developed according to psychologistic criterion should guide the deductive model. The method is compared to other ones presented in the literature on logical omniscience such as Hintikka’s and Vinkov and Fominuh. Views from different perspectives such as computer science and artificial intelligence are also provided.

Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.

Gaussoids are two-antecedental approximations of Gaussian conditional independence structures

The gaussoid axioms are conditional independence inference rules which characterize regular Gaussian CI structures over a three-element ground set. It is known that no finite set of inference rules completely describes regular Gaussian CI as the ground set grows. In this article we show that the gaussoid axioms logically imply every inference rule of at most two antecedents which is valid for regular Gaussians over any ground set. The proof is accomplished by exhibiting for each inclusion-minimal gaussoid extension of at most two CI statements a regular Gaussian realization. Moreover we prove that all those gaussoids have rational positive-definite realizations inside every ε-ball around the identity matrix. For the proof we introduce the concept of algebraic Gaussians over arbitrary fields and of positive Gaussians over ordered fields and obtain the same two-antecedental completeness of the gaussoid axioms for algebraic and positive Gaussians over all fields of characteristic zero as a byproduct.

Detecting Vicious Cycles in Urban Problem Knowledge Graph using Inference Rules

Urban areas have many problems, including homelessness, graffiti, and littering. These problems are influenced by various factors and are linked to each other; thus, an understanding of the problem structure is required in order to detect and solve the root problems that generate vicious cycles. Moreover, before implementing action plans to solve these problems, local governments need to estimate cost-effectiveness when the plans are carried out. Therefore, this paper proposes constructing an urban problem knowledge graph that would include urban problems' causality and the related cost information in budget sheets. In addition, this paper proposes a method for detecting vicious cycles of urban problems using SPARQL queries with inference rules from the knowledge graph. Finally, several root problems that led to vicious cycles were detected. Urban-problem experts evaluated the extracted causal relations.

Sequent Systems without Improper Derivations

In the natural deduction system for classical propositional logic given by G. Gentzen, there are some inference rules with assumptions discharged by the rule. D. Prawitz calls such inference rules improper, and others proper. Improper inference rules are more complicated and are often harder to understand than the proper ones. In the present paper, we distinguish between proper and improper derivations by using sequent systems. Specifically, we introduce a sequent system \(\vdash_{\bf Sc}\) for classical propositional logic with only structural rules, and prove that \(\vdash_{\bf Sc}\) does not allow improper derivations in general. For instance, the sequent \(\Rightarrow p \to q\) cannot be derived from the sequent \(p \Rightarrow q\) in \(\vdash_{\bf Sc}\). In order to prove the failure of improper derivations, we modify the usual notion of truth valuation, and using the modified valuation, we prove the completeness of \(\vdash_{\bf Sc}\). We also consider whether an improper derivation can be described generally by using \(\vdash_{\bf Sc}\).

Foundations of regular coinduction

Inference systems are a widespread framework used to define possibly recursive predicates by means of inference rules. They allow both inductive and coinductive interpretations that are fairly well-studied. In this paper, we consider a middle way interpretation, called regular, which combines advantages of both approaches: it allows non-well-founded reasoning while being finite. We show that the natural proof-theoretic definition of the regular interpretation, based on regular trees, coincides with a rational fixed point. Then, we provide an equivalent inductive characterization, which leads to an algorithm which looks for a regular derivation of a judgment. Relying on these results, we define proof techniques for regular reasoning: the regular coinduction principle, to prove completeness, and an inductive technique to prove soundness, based on the inductive characterization of the regular interpretation. Finally, we show the regular approach can be smoothly extended to inference systems with corules, a recently introduced, generalised framework, which allows one to refine the coinductive interpretation, proving that also this flexible regular interpretation admits an equivalent inductive characterisation.

Fuzzy Implementation in The Selection of A Chieving Employees at PT. Sumber Barkah using Matlab Software

A company must set a high standard of discipline so that the company can develop quickly. A good company cannot be separated from the performance of employees in the form of standard rules made. With the standard, the company can see employees who excel and can be used as examples for other employees. There are 3 generated criteria such as performance, target and absence. The main purpose of this study is to provide criteria for selecting outstanding employees in a company. This study uses mamdani which uses the lowest min value and uses the AND operator to get the results. There are four things in the Mamdani fuzzy process, the first is the fuzification of the determination of the input value, the second is the application of the implication function, the third is the inference rules and the last is defuzzification. The results of this study can be used as a standard in determining outstanding employees at PT Berkah

Superposition with Lambdas

We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $$\beta \eta $$ β η -equivalence classes of $$\lambda $$ λ -terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.

Carnap and Beth on the Limits of Tolerance

Rudolf Carnap’s principle of tolerance states that there is no need to justify the adoption of a logic by philosophical means. Carnap uses the freedom provided by this principle in his philosophy of mathematics: he wants to capture the idea that mathematical truth is a matter of linguistic rules by relying on a strong metalanguage with infinitary inference rules. In this paper, I give a new interpretation of an argument by E. W. Beth, which shows that the principle of tolerance does not suffice to remove all obstacles to the employment of infinitary rules.