scholarly journals Tableau Calculus for Dummett Logic Based on Present and Next State of Knowledge

10.29007/dhz5 ◽  
2018 ◽  
Author(s):  
Guido Fiorino
Keyword(s):  
Intuitionistic Logic ◽  
Search Space ◽  
Kripke Semantics ◽  
Proof Systems ◽  
Dummett Logic ◽  
Intermediate Logics ◽  
Tableau System

In this paper we use the Kripke semantics characterization of Dummett logic to introduce a new way of handling non-forced formulas in tableau proof systems. We pursue the aim of reducing the search space by strictly increasing the number of forced propositional variables after the application of non-invertible rules. The focus of the paper is on a new tableau system for Dummett logic, for which we have an implementation. The ideas presented can be extended to intuitionistic logic and intermediate logics as well.

scholarly journals Applications of intuitionistic logic in Answer Set Programming

2004 ◽  
Vol 4 (3) ◽  
pp. 325-354 ◽  
Author(s):  
MAURICIO OSORIO ◽  
JUAN A. NAVARRO ◽  
JOSÉ ARRAZOLA
Keyword(s):  
Recent Result ◽  
Intuitionistic Logic ◽  
Answer Set Programming ◽  
Minimal Models ◽  
Logic Programs ◽  
Intermediate Logics ◽  
Answer Set Semantics ◽  
Answer Sets ◽  
Answer Set

We present some applications of intermediate logics in the field of Answer Set Programming (ASP). A brief, but comprehensive introduction to the answer set semantics, intuitionistic and other intermediate logics is given. Some equivalence notions and their applications are discussed. Some results on intermediate logics are shown, and applied later to prove properties of answer sets. A characterization of answer sets for logic programs with nested expressions is provided in terms of intuitionistic provability, generalizing a recent result given by Pearce. It is known that the answer set semantics for logic programs with nested expressions may select non-minimal models. Minimal models can be very important in some applications, therefore we studied them; in particular we obtain a characterization, in terms of intuitionistic logic, of answer sets which are also minimal models. We show that the logic G3 characterizes the notion of strong equivalence between programs under the semantic induced by these models. Finally we discuss possible applications and consequences of our results. They clearly state interesting links between ASP and intermediate logics, which might bring research in these two areas together.

scholarly journals Very Fast and Accurate Procedure for the Characterization of Photovoltaic Panels from Datasheet Information

2014 ◽  
Vol 2014 ◽  
pp. 1-10 ◽  
Author(s):  
Antonino Laudani ◽  
Francesco Riganti Fulginei ◽  
Alessandro Salvini ◽  
Gabriele Maria Lozito ◽  
Salvatore Coco
Keyword(s):  
Numerical Methods ◽  
Search Space ◽  
Extraction Process ◽  
Reduced Form ◽  
Photovoltaic Panels ◽  
Approximation Techniques ◽  
Computational Costs ◽  
Minimization Technique ◽  
Accurate Procedure

In recent years several numerical methods have been proposed to identify the five-parameter model of photovoltaic panels from manufacturer datasheets also by introducing simplification or approximation techniques. In this paper we present a fast and accurate procedure for obtaining the parameters of the five-parameter model by starting from its reduced form. The procedure allows characterizing, in few seconds, thousands of photovoltaic panels present on the standard databases. It introduces and takes advantage of further important mathematical considerations without any model simplifications or data approximations. In particular the five parameters are divided in two groups, independent and dependent parameters, in order to reduce the dimensions of the search space. The partitioning of the parameters provides a strong advantage in terms of convergence, computational costs, and execution time of the present approach. Validations on thousands of photovoltaic panels are presented that show how it is possible to make easy and efficient the extraction process of the five parameters, without taking care of choosing a specific solver algorithm but simply by using any deterministic optimization/minimization technique.

scholarly journals A characterization of optimal multiprocessor schedules and new dominance rules

2020 ◽  
Vol 40 (4) ◽  
pp. 876-900
Author(s):  
Rico Walter ◽  
Alexander Lawrinenko
Keyword(s):  
Parallel Machines ◽  
Computational Study ◽  
Search Space ◽  
Point Of View ◽  
Theoretical Point ◽  
Optimal Solutions ◽  
Identical Parallel Machines ◽  
Makespan Minimization ◽  
Structural Pattern

Abstract The paper on hand approaches the classical makespan minimization problem on identical parallel machines from a rather theoretical point of view. Using an approach similar to the idea behind inverse optimization, we identify a general structural pattern of optimal multiprocessor schedules. We also show how to derive new dominance rules from the characteristics of optimal solutions. Results of our computational study attest to the efficacy of the new rules. They are particularly useful in limiting the search space when each machine processes only a few jobs on average.

scholarly journals Variability Map of Objective Function for Analysis of Global Optimization Problem Characteristic Features

2019 ◽  
pp. 4-21
Author(s):  
T.A. Agasiev
Keyword(s):  
Objective Function ◽  
Information Content ◽  
Optimization Problem ◽  
Target Function ◽  
Search Space ◽  
Experiment Design ◽  
Generalized Information ◽  
Problem Characteristic ◽  
Characteristic Features

Methods of landscape analysis are developed to estimate various characteristic features of the objective function in the optimization problem. The accuracy of the estimates largely depends on the chosen method of experiment design for the landscape sampling, i.e. on the number and location of points in the search space forming a discrete representation of the objective function landscape. The method of information content is the most resistant to changes in the experiment design but requires route building to bypass the obtained points of landscape sampling. A method of characterization of the optimization problem objective function is proposed on the base of landscape sampling without building a route to bypass its points. The notion of a variability map of objective function is introduced. The informativeness criteria are formulated for groups of points of a landscape sample. A method of constructing the so-called full variability map is proposed as well as the function of generalized information content for the analysis of the characteristic features of the objective function. The method allows obtaining more accurate estimates of target function characteristics which are resistant to variations of the experiment design

scholarly journals Museum of Outstanding Figures in Ukrainian Culture

2022 ◽  
pp. 1-10
Author(s):  
Iaroslav Petik
Keyword(s):  
Artificial Intelligence ◽  
Bounded Rationality ◽  
Intuitionistic Logic ◽  
Informal Logic ◽  
Logical Omniscience ◽  
Human Reasoning ◽  
Inference Rules ◽  
Philosophy Of Psychology ◽  
Psychological Mechanisms

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.

ON FLATTENING ELIMINATION RULES

2014 ◽  
Vol 7 (1) ◽  
pp. 60-72 ◽  
Author(s):  
GRIGORY K. OLKHOVIKOV ◽  
PETER SCHROEDER-HEISTER
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Second Order ◽  
Kripke Semantics ◽  
Elimination Rule

AbstractIn proof-theoretic semantics of intuitionistic logic it is well known that elimination rules can be generated from introduction rules in a uniform way. If introduction rules discharge assumptions, the corresponding elimination rule is a rule of higher level, which allows one to discharge rules occurring as assumptions. In some cases, these uniformly generated elimination rules can be equivalently replaced with elimination rules that only discharge formulas or do not discharge any assumption at all—they can be flattened in a terminology proposed by Read. We show by an example from propositional logic that not all introduction rules have flat elimination rules. We translate the general form of flat elimination rules into a formula of second-order propositional logic and demonstrate that our example is not equivalent to any such formula. The proof uses elementary techniques from propositional logic and Kripke semantics.

Sign in / Sign up

Export Citation Format

Share Document