TY - BOOK A1 - Seuring, Markus A1 - Gössel, Michael A1 - Sogomonyan, Egor S. T1 - A structural approach for space compaction for concurrent checking and BIST T3 - Preprint / Universität Potsdam, Institut für Informatik Y1 - 1997 SN - 0946-7580 VL - 1997, 01 PB - Univ. Potsdam CY - Potsdam [u.a.] ER - TY - JOUR A1 - Gössel, Michael A1 - Sogomonyan, Egor S. T1 - On-line Test auf der Grundlage eines die Parität erhaltenden Signaturanalysators Y1 - 1998 ER - TY - JOUR A1 - Morosov, Andrej A1 - Saposhnikov, V. V. A1 - Gössel, Michael T1 - Self-Checking circuits with unidiectionally independent outputs Y1 - 1998 ER - TY - JOUR A1 - Krstić, Miloš A1 - Weidling, Stefan A1 - Petrovic, Vladimir A1 - Sogomonyan, Egor S. T1 - Enhanced architectures for soft error detection and correction in combinational and sequential circuits JF - Microelectronics Reliability N2 - In this paper two new methods for the design of fault-tolerant pipelined sequential and combinational circuits, called Error Detection and Partial Error Correction (EDPEC) and Full Error Detection and Correction (FEDC), are described. The proposed methods are based on an Error Detection Logic (EDC) in the combinational circuit part combined with fault tolerant memory elements implemented using fault tolerant master–slave flip-flops. If a transient error, due to a transient fault in the combinational circuit part is detected by the EDC, the error signal controls the latching stage of the flip-flops such that the previous correct state of the register stage is retained until the transient error disappears. The system can continue to work in its previous correct state and no additional recovery procedure (with typically reduced clock frequency) is necessary. The target applications are dataflow processing blocks, for which software-based recovery methods cannot be easily applied. The presented architectures address both single events as well as timing faults of arbitrarily long duration. An example of this architecture is developed and described, based on the carry look-ahead adder. The timing conditions are carefully investigated and simulated up to the layout level. The enhancement of the baseline architecture is demonstrated with respect to the achieved fault tolerance for the single event and timing faults. It is observed that the number of uncorrected single events is reduced by the EDPEC architecture by 2.36 times compared with previous solution. The FEDC architecture further reduces the number of uncorrected events to zero and outperforms the Triple Modular Redundancy (TMR) with respect to correction of timing faults. The power overhead of both new architectures is about 26–28% lower than the TMR. Y1 - 2016 SN - 0026-2714 VL - 56 SP - 212 EP - 220 ER - TY - THES A1 - Klockmann, Alexander T1 - Modifizierte Unidirektionale Codes für Speicherfehler N2 - Das Promotionsvorhaben verfolgt das Ziel, die Zuverlässigkeit der Datenspeicherung und die Speicherdichte von neu entwickelten Speichern (Emerging Memories) mit Multi-Level-Speicherzellen zu verbessern bzw. zu erhöhen. Hierfür werden Codes zur Erkennung von unidirektionalen Fehlern analysiert, modifiziert und neu entwickelt, um sie innerhalb der neuen Speicher anwenden zu können. Der Fokus liegt dabei auf sog. Berger-Codes und m-aus-n-Codes. Da Multi-Level-Speicherzellen nicht mehr binär, sondern mit mehreren Leveln arbeiten, können bisher verwendete Codes nicht mehr verwendet werden, bzw. müssen entsprechend angepasst werden. Auf Basis der Berger-Codes und m-aus-n-Codes werden in dieser Arbeit neue Codes abgeleitet, welche in der Lage sind, Daten auch in mehrwertigen Systemen zu schützen. KW - Fehlererkennung KW - Codierungstheorie KW - Speicher KW - unidirektionale Fehler Y1 - 2022 ER - TY - JOUR A1 - Schick, Daniel A1 - Bojahr, Andre A1 - Herzog, Marc A1 - Shayduk, Roman A1 - von Korff Schmising, Clemens A1 - Bargheer, Matias T1 - Udkm1Dsim-A simulation toolkit for 1D ultrafast dynamics in condensed matter JF - Computer physics communications : an international journal devoted to computational physics and computer programs in physics N2 - The UDKM1DSIM toolbox is a collection of MATLAB (MathWorks Inc.) classes and routines to simulate the structural dynamics and the according X-ray diffraction response in one-dimensional crystalline sample structures upon an arbitrary time-dependent external stimulus, e.g. an ultrashort laser pulse. The toolbox provides the capabilities to define arbitrary layered structures on the atomic level including a rich database of corresponding element-specific physical properties. The excitation of ultrafast dynamics is represented by an N-temperature model which is commonly applied for ultrafast optical excitations. Structural dynamics due to thermal stress are calculated by a linear-chain model of masses and springs. The resulting X-ray diffraction response is computed by dynamical X-ray theory. The UDKM1DSIM toolbox is highly modular and allows for introducing user-defined results at any step in the simulation procedure. Program summary Program title: udkm1Dsim Catalogue identifier: AERH_v1_0 Program summary URL: http://cpc.cs.qub.ac.uk/summaries/AERH_v1_0.html Licensing provisions: BSD No. of lines in distributed program, including test data, etc.: 130221 No. of bytes in distributed program, including test data, etc.: 2746036 Distribution format: tar.gz Programming language: Matlab (MathWorks Inc.). Computer: PC/Workstation. Operating system: Running Matlab installation required (tested on MS Win XP -7, Ubuntu Linux 11.04-13.04). Has the code been vectorized or parallelized?: Parallelization for dynamical XRD computations. Number of processors used: 1-12 for Matlab Parallel Computing Toolbox; 1 - infinity for Matlab Distributed Computing Toolbox External routines: Optional: Matlab Parallel Computing Toolbox, Matlab Distributed Computing Toolbox Required (included in the package): mtimesx Fast Matrix Multiply for Matlab by James Tursa, xml io tools by Jaroslaw Tuszynski, textprogressbar by Paul Proteus Nature of problem: Simulate the lattice dynamics of 1D crystalline sample structures due to an ultrafast excitation including thermal transport and compute the corresponding transient X-ray diffraction pattern. Solution method: Restrictions: The program is restricted to 1D sample structures and is further limited to longitudinal acoustic phonon modes and symmetrical X-ray diffraction geometries. Unusual features: The program is highly modular and allows the inclusion of user-defined inputs at any time of the simulation procedure. Running time: The running time is highly dependent on the number of unit cells in the sample structure and other simulation parameters such as time span or angular grid for X-ray diffraction computations. However, the example files are computed in approx. 1-5 min each on a 8 Core Processor with 16 GB RAM available. KW - Ultrafast dynamics KW - Heat diffusion KW - N-temperature model KW - Coherent phonons KW - Incoherent phonons KW - Thermoelasticity KW - Dynamical X-ray theory Y1 - 2014 U6 - https://doi.org/10.1016/j.cpc.2013.10.009 SN - 0010-4655 SN - 1879-2944 VL - 185 IS - 2 SP - 651 EP - 660 PB - Elsevier CY - Amsterdam ER - TY - GEN A1 - Fandiño, Jorge T1 - Founded (auto)epistemic equilibrium logic satisfies epistemic splitting T2 - Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe N2 - In a recent line of research, two familiar concepts from logic programming semantics (unfounded sets and splitting) were extrapolated to the case of epistemic logic programs. The property of epistemic splitting provides a natural and modular way to understand programs without epistemic cycles but, surprisingly, was only fulfilled by Gelfond's original semantics (G91), among the many proposals in the literature. On the other hand, G91 may suffer from a kind of self-supported, unfounded derivations when epistemic cycles come into play. Recently, the absence of these derivations was also formalised as a property of epistemic semantics called foundedness. Moreover, a first semantics proved to satisfy foundedness was also proposed, the so-called Founded Autoepistemic Equilibrium Logic (FAEEL). In this paper, we prove that FAEEL also satisfies the epistemic splitting property something that, together with foundedness, was not fulfilled by any other approach up to date. To prove this result, we provide an alternative characterisation of FAEEL as a combination of G91 with a simpler logic we called Founded Epistemic Equilibrium Logic (FEEL), which is somehow an extrapolation of the stable model semantics to the modal logic S5. T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 1060 KW - answer set programming KW - epistemic specifications KW - epistemic logic programs Y1 - 2020 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-469685 SN - 1866-8372 IS - 1060 SP - 671 EP - 687 ER - TY - JOUR A1 - Cabalar, Pedro A1 - Fandiño, Jorge A1 - Fariñas del Cerro, Luis T1 - Splitting epistemic logic programs JF - Theory and practice of logic programming / publ. for the Association for Logic Programming N2 - Epistemic logic programs constitute an extension of the stable model semantics to deal with new constructs called subjective literals. Informally speaking, a subjective literal allows checking whether some objective literal is true in all or some stable models. As it can be imagined, the associated semantics has proved to be non-trivial, since the truth of subjective literals may interfere with the set of stable models it is supposed to query. As a consequence, no clear agreement has been reached and different semantic proposals have been made in the literature. Unfortunately, comparison among these proposals has been limited to a study of their effect on individual examples, rather than identifying general properties to be checked. In this paper, we propose an extension of the well-known splitting property for logic programs to the epistemic case. We formally define when an arbitrary semantics satisfies the epistemic splitting property and examine some of the consequences that can be derived from that, including its relation to conformant planning and to epistemic constraints. Interestingly, we prove (through counterexamples) that most of the existing approaches fail to fulfill the epistemic splitting property, except the original semantics proposed by Gelfond 1991 and a recent proposal by the authors, called Founded Autoepistemic Equilibrium Logic. KW - knowledge representation and nonmonotonic reasoning KW - logic programming methodology and applications KW - theory Y1 - 2021 U6 - https://doi.org/10.1017/S1471068420000058 SN - 1471-0684 SN - 1475-3081 VL - 21 IS - 3 SP - 296 EP - 316 PB - Cambridge Univ. Press CY - Cambridge [u.a.] ER - TY - GEN A1 - Bosser, Anne-Gwenn A1 - Cabalar, Pedro A1 - Dieguez, Martin A1 - Schaub, Torsten H. T1 - Introducing temporal stable models for linear dynamic logic T2 - 16th International Conference on Principles of Knowledge Representation and Reasoning N2 - We propose a new temporal extension of the logic of Here-and-There (HT) and its equilibria obtained by combining it with dynamic logic over (linear) traces. Unlike previous temporal extensions of HT based on linear temporal logic, the dynamic logic features allow us to reason about the composition of actions. For instance, this can be used to exercise fine grained control when planning in robotics, as exemplified by GOLOG. In this paper, we lay the foundations of our approach, and refer to it as Linear Dynamic Equilibrium Logic, or simply DEL. We start by developing the formal framework of DEL and provide relevant characteristic results. Among them, we elaborate upon the relationships to traditional linear dynamic logic and previous temporal extensions of HT. Y1 - 2018 UR - https://www.dc.fi.udc.es/~cabalar/del.pdf SP - 12 EP - 21 PB - ASSOC Association for the Advancement of Artificial Intelligence CY - Palo Alto ER - TY - JOUR A1 - Fandiño, Jorge A1 - Lifschitz, Vladimir A1 - Lühne, Patrick A1 - Schaub, Torsten H. T1 - Verifying tight logic programs with Anthem and Vampire JF - Theory and practice of logic programming N2 - This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas. Y1 - 2020 U6 - https://doi.org/10.1017/S1471068420000344 SN - 1471-0684 SN - 1475-3081 VL - 20 IS - 5 SP - 735 EP - 750 PB - Cambridge Univ. Press CY - Cambridge [u.a.] ER - TY - GEN A1 - Aguado, Felicidad A1 - Cabalar, Pedro A1 - Fandiño, Jorge A1 - Pearce, David A1 - Perez, Gilberto A1 - Vidal, Concepcion T1 - Revisiting explicit negation in answer set programming T2 - Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe N2 - A common feature in Answer Set Programming is the use of a second negation, stronger than default negation and sometimes called explicit, strong or classical negation. This explicit negation is normally used in front of atoms, rather than allowing its use as a regular operator. In this paper we consider the arbitrary combination of explicit negation with nested expressions, as those defined by Lifschitz, Tang and Turner. We extend the concept of reduct for this new syntax and then prove that it can be captured by an extension of Equilibrium Logic with this second negation. We study some properties of this variant and compare to the already known combination of Equilibrium Logic with Nelson's strong negation. T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 1104 KW - Answer Set Programming KW - non-monotonic reasoning KW - Equilibrium logic KW - explicit negation Y1 - 2021 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-469697 SN - 1866-8372 IS - 1104 SP - 908 EP - 924 ER - TY - JOUR A1 - Cabalar, Pedro A1 - Fandiño, Jorge A1 - Garea, Javier A1 - Romero, Javier A1 - Schaub, Torsten H. T1 - Eclingo BT - a solver for epistemic logic programs JF - Theory and practice of logic programming N2 - We describe eclingo, a solver for epistemic logic programs under Gelfond 1991 semantics built upon the Answer Set Programming system clingo. The input language of eclingo uses the syntax extension capabilities of clingo to define subjective literals that, as usual in epistemic logic programs, allow for checking the truth of a regular literal in all or in some of the answer sets of a program. The eclingo solving process follows a guess and check strategy. It first generates potential truth values for subjective literals and, in a second step, it checks the obtained result with respect to the cautious and brave consequences of the program. This process is implemented using the multi-shot functionalities of clingo. We have also implemented some optimisations, aiming at reducing the search space and, therefore, increasing eclingo 's efficiency in some scenarios. Finally, we compare the efficiency of eclingo with two state-of-the-art solvers for epistemic logic programs on a pair of benchmark scenarios and show that eclingo generally outperforms their obtained results. KW - Answer Set Programming KW - Epistemic Logic Programs KW - Non-Monotonic KW - Reasoning KW - Conformant Planning Y1 - 2020 U6 - https://doi.org/10.1017/S1471068420000228 SN - 1471-0684 SN - 1475-3081 VL - 20 IS - 6 SP - 834 EP - 847 PB - Cambridge Univ. Press CY - New York ER - TY - THES A1 - Frank, Mario T1 - On synthesising Linux kernel module components from Coq formalisations T1 - Über die Synthese von Linux Kernel- Modul-Komponenten aus Coq-Formalisierungen N2 - This thesis presents an attempt to use source code synthesised from Coq formalisations of device drivers for existing (micro)kernel operating systems, with a particular focus on the Linux Kernel. In the first part, the technical background and related work are described. The focus is here on the possible approaches to synthesising certified software with Coq, namely the extraction to functional languages using the Coq extraction plugin and the extraction to Clight code using the CertiCoq plugin. It is noted that the implementation of CertiCoq is verified, whereas this is not the case for the Coq extraction plugin. Consequently, there is a correctness guarantee for the generated Clight code which does not hold for the code being generated by the Coq extraction plugin. Furthermore, the differences between user space and kernel space software are discussed in relation to Linux device drivers. It is elaborated that it is not possible to generate working Linux kernel module components using the Coq extraction plugin without significant modifications. In contrast, it is possible to produce working user space drivers both with the Coq extraction plugin and CertiCoq. The subsequent parts describe the main contributions of the thesis. In the second part, it is demonstrated how to extend the Coq extraction plugin to synthesise foreign function calls between the functional language OCaml and the imperative language C. This approach has the potential to improve the type-safety of user space drivers. Furthermore, it is shown that the code being synthesised by CertiCoq cannot be used in kernel space without modifications to the necessary runtime. Consequently, the necessary modifications to the runtimes of CertiCoq and VeriFFI are introduced, resulting in the runtimes becoming compatible components of a Linux kernel module. Furthermore, justifications for the transformations are provided and possible further extensions to both plugins and solutions to failing garbage collection calls in kernel space are discussed. The third part presents a proof of concept device driver for the Linux Kernel. To achieve this, the event handler of the original PC Speaker driver is partially formalised in Coq. Furthermore, some relevant formal properties of the formalised functionality are discussed. Subsequently, a kernel module is defined, utilising the modified variants of CertiCoq and VeriFFI to compile a working device driver. It is furthermore shown that it is possible to compile the synthesised code with CompCert, thereby extending the guarantee of correctness to the assembly layer. This is followed by a performance evaluation that compares a naive formalisation of the PC speaker functionality with the original PC Speaker driver pointing out the weaknesses in the formalisation and possible improvements. The part closes with a summary of the results, their implications and open questions being raised. The last part lists all used sources, separated into scientific literature, documentations or reference manuals and artifacts, i.e. source code. N2 - Die vorliegende Dissertation präsentiert einen Ansatz zur Nutzung von Quellcode, der aus der Coq-Formalisierung eines Gerätetreibers generiert wurde, für bestehende (Mikrokernel-)Betriebssysteme, im Speziellen den Linux-Kernel. Im ersten Teil erfolgt eine Beschreibung der relevanten technischen Aspekte sowie des aktuellen Forschungsstandes. Dabei liegt der Fokus auf der Synthese von funktionalem Code durch das Coq Extraction Plugin und von Clight Code durch das CertiCoq Plugin. Des Weiteren wird dargelegt, dass die Implementierung von CertiCoq im Gegensatz zu der des Coq Extraction Plugin verifiziert ist, wodurch sich eine Korrektheitsgarantie für den generierten Clight Code ableiten lässt. Darüber hinaus werden die Unterschiede zwischen User Space und Kernel Space Software in Bezug auf Linux-Treiber erörtert. Unter Berücksichtigung der technischen Einschränkungen wird dargelegt, dass der durch das Coq Extraction Plugin generierte Code ohne gravierende Anpassungen der Laufzeitumgebung nicht als Teil eines Kernel Space Treibers nutzbar ist. Die nachfolgenden Teile der Dissertation behandeln den Beitrag dieser Arbeit. Im zweiten Teil wird dargelegt, wie das Coq Extraction Plugin derart erweitert werden kann, dass typsichere Aufrufe zwischen den Sprachen OCaml und C generiert werden können. Dies verhindert spezifische Kompilationsfehler aufgrund von Typfehlern. Des Weiteren wird aufgezeigt, dass der durch CertiCoq generierte Code ebenfalls nicht im Kernel Space genutzt werden kann, da die Laufzeitumgebung technische Einschränkungen verletzt. Daher werden die notwendigen Anpassungen an der vergleichsweise kleinen Laufzeitumgebung sowie an VeriFFI vorgestellt und deren Korrektheit begründet. Anschließend werden mögliche Erweiterungen beider Plugins sowie die Möglichkeit der Behandlung von fehlschlagenden Aufrufen der Garbage Collection von CertiCoq im Kernel Space erörtert. Im dritten Teil wird als Machbarkeitsstudie im ersten Schritt der Event-Handler des Linux PC Speaker Treibers beschrieben und eine naive Coq-Formalisierung sowie wichtige formale Eigenschaften dargelegt. Dann wird beschrieben, wie ein Kernel-Modul und dessen Kompilation definiert werden muss, um einen lauffähigen Linux Kernel Treiber zu erhalten. Des Weiteren wird erläutert, wie die generierten Teile dieses Treibers mit dem verifizierten Kompiler CompCert übersetzt werden können, wodurch auch eine Korrektheit für den resultierenden Assembler-Code gilt. Im Anschluss erfolgt eine Evaluierung der Performance des aus der naiven Coq-Formalisierung generierten Codes im Vergleich zum originalen PC-Speaker Treiber. Dabei werden die Schwächen der Formalisierung sowie mögliche Verbesserungen diskutiert. Der Teil wird mit einer Zusammenfassung der Ergebnisse sowie der daraus resultierenden offenen Fragen abgeschlossen. Der letzte Teil gibt eine Übersicht über genutzte Quellen und Hilfsmittel, unterteilt in wissenschaftliche Literatur, Dokumentationen sowie Software-Artefakte. KW - Linux device drivers KW - Coq KW - CertiCoq KW - synthesis KW - compilation KW - Geräte-Treiber KW - Linux KW - Coq KW - CertiCoq KW - Synthese KW - Kompilation Y1 - 2024 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-642558 ER - TY - JOUR A1 - Roessner, Ute A1 - Luedemann, A. A1 - Brust, D. A1 - Fiehn, Oliver A1 - Linke, Thomas A1 - Willmitzer, Lothar A1 - Fernie, Alisdair R. T1 - Metabolic profiling allows comprehensive phenotyping of genetically or environmentally modified plant systems Y1 - 2001 SN - 1040-4651 ER - TY - JOUR A1 - Cabalar, Pedro A1 - Fandiño, Jorge A1 - Schaub, Torsten H. A1 - Schellhorn, Sebastian T1 - Gelfond-Zhang aggregates as propositional formulas JF - Artificial intelligence N2 - Answer Set Programming (ASP) has become a popular and widespread paradigm for practical Knowledge Representation thanks to its expressiveness and the available enhancements of its input language. One of such enhancements is the use of aggregates, for which different semantic proposals have been made. In this paper, we show that any ASP aggregate interpreted under Gelfond and Zhang's (GZ) semantics can be replaced (under strong equivalence) by a propositional formula. Restricted to the original GZ syntax, the resulting formula is reducible to a disjunction of conjunctions of literals but the formulation is still applicable even when the syntax is extended to allow for arbitrary formulas (including nested aggregates) in the condition. Once GZ-aggregates are represented as formulas, we establish a formal comparison (in terms of the logic of Here-and-There) to Ferraris' (F) aggregates, which are defined by a different formula translation involving nested implications. In particular, we prove that if we replace an F-aggregate by a GZ-aggregate in a rule head, we do not lose answer sets (although more can be gained). This extends the previously known result that the opposite happens in rule bodies, i.e., replacing a GZ-aggregate by an F-aggregate in the body may yield more answer sets. Finally, we characterize a class of aggregates for which GZ- and F-semantics coincide. KW - Aggregates KW - Answer Set Programming Y1 - 2019 U6 - https://doi.org/10.1016/j.artint.2018.10.007 SN - 0004-3702 SN - 1872-7921 VL - 274 SP - 26 EP - 43 PB - Elsevier CY - Amsterdam ER - TY - JOUR A1 - Aguado, Felicidad A1 - Cabalar, Pedro A1 - Fandiño, Jorge A1 - Pearce, David A1 - Perez, Gilberto A1 - Vidal, Concepcion T1 - Forgetting auxiliary atoms in forks JF - Artificial intelligence N2 - In this work we tackle the problem of checking strong equivalence of logic programs that may contain local auxiliary atoms, to be removed from their stable models and to be forbidden in any external context. We call this property projective strong equivalence (PSE). It has been recently proved that not any logic program containing auxiliary atoms can be reformulated, under PSE, as another logic program or formula without them – this is known as strongly persistent forgetting. In this paper, we introduce a conservative extension of Equilibrium Logic and its monotonic basis, the logic of Here-and-There, in which we deal with a new connective ‘|’ we call fork. We provide a semantic characterisation of PSE for forks and use it to show that, in this extension, it is always possible to forget auxiliary atoms under strong persistence. We further define when the obtained fork is representable as a regular formula. KW - Answer set programming KW - Non-monotonic reasoning KW - Equilibrium logic KW - Denotational semantics KW - Forgetting KW - Strong equivalence Y1 - 2019 U6 - https://doi.org/10.1016/j.artint.2019.07.005 SN - 0004-3702 SN - 1872-7921 VL - 275 SP - 575 EP - 601 PB - Elsevier CY - Amsterdam ER - TY - GEN A1 - Cabalar, Pedro A1 - Fandiño, Jorge A1 - Schaub, Torsten H. A1 - Schellhorn, Sebastian T1 - Lower Bound Founded Logic of Here-and-There T2 - Logics in Artificial Intelligence N2 - A distinguishing feature of Answer Set Programming is that all atoms belonging to a stable model must be founded. That is, an atom must not only be true but provably true. This can be made precise by means of the constructive logic of Here-and-There, whose equilibrium models correspond to stable models. One way of looking at foundedness is to regard Boolean truth values as ordered by letting true be greater than false. Then, each Boolean variable takes the smallest truth value that can be proven for it. This idea was generalized by Aziz to ordered domains and applied to constraint satisfaction problems. As before, the idea is that a, say integer, variable gets only assigned to the smallest integer that can be justified. In this paper, we present a logical reconstruction of Aziz’ idea in the setting of the logic of Here-and-There. More precisely, we start by defining the logic of Here-and-There with lower bound founded variables along with its equilibrium models and elaborate upon its formal properties. Finally, we compare our approach with related ones and sketch future work. Y1 - 2019 SN - 978-3-030-19570-0 SN - 978-3-030-19569-4 U6 - https://doi.org/10.1007/978-3-030-19570-0_34 SN - 0302-9743 SN - 1611-3349 VL - 11468 SP - 509 EP - 525 PB - Springer CY - Cham ER - TY - JOUR A1 - Aguado, Felicidad A1 - Cabalar, Pedro A1 - Fandiño, Jorge A1 - Pearce, David A1 - Perez, Gilberto A1 - Vidal-Peracho, Concepcion T1 - Revisiting Explicit Negation in Answer Set Programming JF - Theory and practice of logic programming KW - Answer set programming KW - Non-monotonic reasoning KW - Equilibrium logic KW - Explicit negation Y1 - 2019 U6 - https://doi.org/10.1017/S1471068419000267 SN - 1471-0684 SN - 1475-3081 VL - 19 IS - 5-6 SP - 908 EP - 924 PB - Cambridge Univ. Press CY - New York ER -