bluuebunny/crossref_metadata_2025 huggingface dataset:
PENDIDIKAN KARAKTER DALAM MATA PELAJARAN PENDIDIKAN AGAMA ISLAM DI SMP 3 PEKALONGAN (Kajian atas Kurikulum dan Proses Pembelajaran)
Authors: Maemonah .
Published: January 2018

Even though character building as an autonomous subject among student does not exist in secondary school, Islamic Education (PAI), as one of the subjects in school related to character building, has to play its role in building students’ character. This study aims to reveal the problems related to PAI learning process in SMP 3 and its role in building students’ noble character. This study was qualitative using observational case studies. The data were obtained through interviews, questionnaires, and documents and were analyzed using qualitative analysis techniques with the inductive approach. The documents were such legal decisions of officials in Educational Ministry, the syllabi, curriculums, and teaching planning (RPP). The result shows that PAI learning has an important role in building students’ noble character if it is supported by competent lecturers, good inputs, adequate materials, and good processes. Character building learning was taught integrated and aimed to shape noble character among the students of SMP 3 Pekalongan. It was accommodated in PAI learning, citizenship learning and local contain subject, such as Javanese language and Cookery Learning. Unfortunately, the sustainability and comprehensiveness of character building learning in PAI curriculum were not seriously attended. Nevertheless, they were taught integrated in pilot project program and evaluated gradually and comprehensively.
MODERNITAS DALAM PERSPEKTIF SEYYED HOSSEIN NASR
Authors: Haryati Tri Astutik
Published: January 2018

This study examined the thought of Seyyed Hossein Nasr on modernity. Nasr confronted Western Metaphysics’ view on one side and Islamic Metaphysics’ view on the other. Nasr took more emphasis on Sufism, though Nasr himself seemed not yet to the level of a mystic Sufi figures as known in the Islamic world. However, Nasr indeed had his own originality-in certain limits-that he concocted Sufism he mastered with his experience and his study results in the West to find alternative answers to the problems of modern man.
Minimización de los efectos atmosféricos en el índice espectral de la vegetación IVIS
Authors: Paz Pellat Fernando
Published: January 2018

It is essential to minimize atmospheric effects on spectral information of remote sensors from space platforms to avoid under estimation of biophysical variables associated with satellite image data. In this paper, a generic algorithm was developed, based on sound theoretical arguments, to analyze time series ISVI spectral vegetation index (vegetation index based on iso-soil curves), thus avoiding the problems associated with the classic design of vegetation indices, where the spectral signal saturates quickly. The results, when applying the algorithm in pixel time series of AVHRR satellite images, showed that reduction and standardization of atmospheric effects in the ISVI was achieved. Using ISVI maximum values in time series (temporal window), a reasonable approximation to atmospheric conditions with minimum or standardized effects was obtained. In conclusion, although the scheme developed failed to eliminate the atmospheric effect on ISVI entirely, it was reduced to a minimum. The algorithm developed was simple enough for operational use, with regard to atmospheric correction methods using radiative model inversions.
Heuristic Decision-Making for Human-aware Navigation in Domestic Environments
Authors: Kirsch Alexandra
Published: January 2018

Robot navigation in domestic environments is still a challenge. This paper introduces a cognitively inspired decision-making method and an instantiation of it for (local) robot navigation in spatially constrained environments. We compare the method to two existing local planners with respect to efficiency, safety and legibility.
Recursive Definitions of Monadic Functions
Authors: Krauss Alexander
Published: January 2018

Using standard domain-theoretic fixed-points, we present an approach for defining recursive functions that are formulated in monadic style. The method works both in the simple option monad and the state-exception monad of Isabelle/HOL's imperative programming extension, which results in a convenient definition principle for imperative programs, which were previously hard to define.

For such monadic functions, the recursion equation can always be derived without preconditions, even if the function is partial. The construction is easy to automate, and convenient induction principles can be derived automatically.
First-Order Interpolation and Interpolating Proof Systems
Authors: Kovács Laura , Voronkov Andrei
Published: January 2018

It is known that one can extract Craig interpolants from so-called local

proofs. An interpolant extracted from such a proof is a boolean

combination of formulas occurring in the proof. However, standard complete

proof systems, such as superposition, for theories having the interpolation

property are not necessarily complete for local proofs: there are formulas

having non-local proofs but no local proof.

In this paper we investigate interpolant extraction from non-local refutations

(proofs of contradiction) in the superposition calculus and prove a number

of general results about interpolant extraction and complexity of extracted

interpolants. In particular, we prove that the number of quantifier alternations

in first-order interpolants of formulas without quantifier alternations is

unbounded. This result has far-reaching consequences for using local proofs

as a foundation for interpolating proof systems: any such proof system should

deal with formulas of arbitrary quantifier complexity.

To search for alternatives for interpolating proof systems, we consider several

variations on interpolation and local proofs. Namely, we give an algorithm for

building interpolants from resolution refutations in logic without equality and

discuss additional constraints when this approach can be also used for logic

with equality. We finally propose a new direction related to interpolation via

local proofs in first-order theories.
iDQ: Instantiation-Based DQBF Solving
Authors: Fröhlich Andreas , Kovásznai Gergely , Biere Armin , Veith Helmut
Published: January 2018

Dependency Quantified Boolean Formulas (DQBF) are obtained by adding Henkin quantifiers to Boolean formulas and have seen growing interest in the last years. Since deciding DQBF is NEXPTIME-complete, efficient ways of solving it would have many practical applications. Still, there is only few work on solving this kind of formulas in practice. In this paper, we present an instantiation-based technique to solve DQBF efficiently. Apart from providing a theoretical foundation, we also propose a concrete implementation of our algorithm. Finally, we give a detailed experimental analysis evaluating our prototype iDQ on several DQBF as well as QBF benchmarks.
A Resolution Method for Modal Logic S5
Authors: Salhi Yakoub , Sioutis Michael
Published: January 2018

The aim of this work is to define a resolution method for the modal logic S5. We

first propose a conjunctive normal form (S5-CNF) which is mainly based on using labels

referring to semantic worlds. In a sense, S5-CNF can be seen as a generalization of the

conjunctive normal form in propositional logic by using in the clause structure the modal

connective of necessity and labels. We show that every S5 formula can be transformed

into an S5-CNF formula using a linear encoding. Then, in order to show the suitability

of our normal form, we describe a modeling of the problem of graph coloring. Finally, we

introduce a simple resolution method for S5, composed of three deductive rules, and we

show that it is sound and complete. Our deductive rules can be seen as adaptations of

Robinson’s resolution rule to the possible-worlds semantics.
Benchmark: DC-to-DC Switched-Mode Power Converters (Buck Converters, Boost Converters, and Buck-Boost Converters)
Authors: Nguyen Luan Viet , Johnson Taylor T
Published: January 2018

Power electronics represent a large and important class of hybrid systems, as modern digital computers and many other systems rely on their correct operation. In this benchmark description, we model three DC-to-DC switched-mode power converters as hybrid automata with continuous dynamics specified by linear ordinary differential equations. A DC-to-DC converter transforms a DC source voltage from one voltage level to another utilizing switches toggled at some (typically kilohertz) frequency with some duty cycle. The state of this switch gives rise to the locations of the hybrid automaton, and the continuous variables are currents and voltages. The main contributions of this benchmark description include: (a) unified modeling of three types of converters as a hybrid automaton with two locations and differing continuous dynamics, and (b) a basic benchmark generator that allows for simulation of these converters in Simulink/Stateflow and reachability analysis in SpaceEx. Future challenges for these benchmark classes include closed-loop control, where the speeds of plant and controller dynamics differ by orders of magnitude.
Beyond DRAT: Challenges in Certifying UNSAT
Authors: Felgenhauer Bertram
Published: January 2018

Contemporary SAT solvers are complex tools and may contain bugs. In

order to increase the trust in the results of SAT solving, SAT solvers

may produce certificates that can be checked independently. For

unsatisfiability certificates, DRAT is the de facto standard. As long

as the checkers are not formalized, extending the certificate format

would decrease the trust in the checker because its code complexity

increases. With the advent of formally verified checkers for DRAT

proofs, this is no longer the case. In this note I argue that

symmetry breaking is not adequately supported by DRAT proofs, and

propose to have dedicated certification for symmetry breaking instead.
When Should Learning Agents Switch to Explicit Knowledge?
Authors: Apeldoorn Daan , Kern-Isberner Gabriele
Published: January 2018

According to psychological models, learned knowledge can be distinguished into implicit and explicit knowledge. The former can be exploited, but cannot be verbalized easily (e.\,g., to explain it to another person). The latter is available in an explicit form, it often comprises generalized, rule-based knowledge which can be verbalized and explained to others. During a learning process, the learned knowledge starts in an implicit form and gets explicit as the learning process progresses, and humans benefit from exploiting such generalized, rule-based knowledge when learning. This paper investigates how learning agents can benefit from explicit knowledge which is extracted during a learning process from a learned implicit representation. It is clearly shown that an agent can already benefit from explicit knowledge in early phases of a learning process.
Proof Support for Common Logic
Authors: Mossakowski Till , Codescu Mihai , Kutz Oliver , Lange Christoph , Grüninger Michael
Published: January 2018

We present the theoretical background for an extension of the Heterogeneous Tool Set Hets that enables proof support for Common Logic. This is achieved via logic translations that relate Common Logic and some of its sublogics to already supported logics and automated theorem proving systems. We thus provide the first theorem proving support for Common Logic covering the full language, including the possibility of verifying meta-theoretical relationships between Common Logic theories.
External Tools for the Formal Proof of the Kepler Conjecture
Authors: Hales Thomas C.
Published: January 2018

The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the familiar cannonball arrangement. The proof of the Kepler conjecture was announced in 1998, but it went several years without publication because of the lingering doubts of referees about the correctness of the proof. In response to these publication hurdles, the Flyspeck project seeks to give a complete formal proof of the Kepler conjecture using the proof assistant HOL Light.

The original proof of the Kepler relies on long computer calculations, and these calculations present special formalization challenges. A major part of the Flyspeck project requires the integration of external computational tools with the proof assistant. Some of these external tools are the GNU linear programming kit, AMPL (a modeling language for mathematical programming), Mathematica calculations, nonlinear optimization, and custom code in C++, C, C#, Java, and Objective Caml.

Earlier work by A. Solovyev has implemented efficient linear programming in HOL Light. This talk will include a description of his more recent work that automates the link between linear programming and the Flyspeck project.
On the Interaction of Inclusion Dependencies with Independence Atoms
Authors: Hannula Miika , Kontinen Juha , Link Sebastian
Published: January 2018

Inclusion dependencies are one of the most important database constraints. In isolation their finite and unrestricted implication problems coincide, are finitely axiomatizable, PSPACE-complete, and fixed-parameter tractable in their arity. In contrast, finite and unrestricted implication problems for the combined class of functional and inclusion de- pendencies deviate from one another and are each undecidable. The same holds true for the class of embedded multivalued dependencies. An important embedded tractable fragment of embedded multivalued dependencies are independence atoms. These stipulate independence between two attribute sets in the sense that for every two tuples there is a third tuple that agrees with the first tuple on the first attribute set and with the second tuple on the second attribute set. For independence atoms, their finite and unrestricted implication problems coincide, are finitely axiomatizable, and decidable in cubic time. In this article, we study the implication problems of the combined class of independence atoms and inclusion dependencies. We show that their finite and unrestricted implication problems coincide, are finitely axiomatizable, PSPACE-complete, and fixed-parameter tractable in their arity. Hence, significant expressivity is gained without sacrificing any of the desirable properties that inclusion dependencies have in isolation. Finally, we establish an efficient condition that is sufficient for independence atoms and inclusion dependencies not to inter- act. The condition ensures that we can apply known algorithms for deciding implication of the individual classes of independence atoms and inclusion dependencies, respectively, to decide implication for an input that combines both individual classes.
A simple and complete model theory for intensional and extensional untyped λ-equality
Authors: Gabbay Michael
Published: January 2018

We present a sound and complete model theory for theories of β-reduction with or without η-expansion. We then show in what conditions we obtain models of β-equality and βη-equality.
Reasoning with Triggers
Authors: Dross Claire , Conchon Sylvain , Kanig Johannes , Paskevich Andrei
Published: January 2018

SMT solvers can decide the satisfiability of ground formulas modulo a combination of

built-in theories. Adding a built-in theory to a given SMT solver is a complex and time consuming task that requires internal knowledge of the solver. However, many theories can be easily expressed using first-order formulas. Unfortunately, since universal quantifiers are not handled in a complete way by SMT solvers, these axiomatics cannot be used as decision procedures.

In this paper, we show how to extend a generic SMT solver to accept a custom theory description and behave as a decision procedure for that theory, provided that the described theory is complete and terminating in a precise sense. The description language consists of first-order axioms with triggers, an instantiation mechanism that is found in many SMT solvers. This mechanism, which usually lacks a clear semantics in existing languages and tools, is rigorously defined here; this definition can be used to prove completeness and termination of the theory. We demonstrate using the theory of arrays, how such proofs can be achieved in our formalism.
A Deductive-Complete Constrained Superposition Calculus for Ground Flat Equational Clauses
Authors: Tourret Sophie , Echenim Mnacho , Peltier Nicolas
Published: January 2018

We describe an algorithm that generates prime implicates of equational clause sets without variables and function symbols. The procedure is based on constrained superposition rules, where constraints are used to store literals that are asserted as additional axioms (or hypotheses) during the proof search. This approach is sound and deductive-complete, and it is more ecient than previous algorithms based on conditional paramodulation. It is also more exible in the sense that it allows one to restrict the search space by imposing additional properties that the generated

implicates should satisfy (e.g., to ensure relevance).
Optimizing Kick Trajectory: A Comparative Study
Authors: Pena Pedro , Masterjohn Joseph , Visser Ubbo
Published: January 2018

Incorporating a dynamic kick engine that is both fast and effective is pivotal to be competitive in one of the world’s biggest AI and robotics initiatives: RoboCup. Using the NAO robot as a testbed, we developed a dynamic kick engine that can generate a kick trajectory with an arbitrary direction without prior input or knowledge of the parameters of the kick. The trajectories are generated using cubic splines (two degree three polynomials with a via-point), cubic Hermite splines or sextics (one six degree polynomial). The trajectories are executed while the robot is dynamically balancing on one foot. Although a variety of kick engines have been implemented by others, there are only a few papers that demonstrate how kick engine parameters have been optimized to give an effective kick or even a kick that minimizes energy consumption and time. Parameters such as kick configuration, limits of the robot, or shape of the polynomial can be optimized. We propose an optimization framework based on the Webots simulator to optimize these parameters. Experiments on different joint interpolators for kick motions have been observed to compare results.
Iterated contraction of propositions and conditionals under the principle of conditional preservation
Authors: Kern-Isberner Gabriele , Bock Tanja , Sauerwald Kai , Beierle Christoph
Published: January 2018

Research on iterated belief change has focussed mostly on belief revision, only few papers have addressed iterated belief contraction. Most prominently, Darwiche and Pearl published seminal work on iterated belief revision the leading paradigm of which is the so-called principle of conditional preservation. In this paper, we use this principle in a thoroughly axiomatized form to develop iterated belief contraction operators for Spohn's ranking functions. We show that it allows for setting up constructive approaches to tackling the problem of how to contract a ranking function by a proposition or a conditional, respectively, and that semantic principles can also be derived from it for the purely qualitative case.
RACCOON: A Connection Reasoner for the Description Logic ALC
Authors: Melo Filho Dimas , Freitas Fred , Otten Jens
Published: January 2018

In this paper, we introduce RACCOON, a reasoner based on the connection calculus ALC θ-CM for the description logic ALC. We describe the calculus, and present details of RACCOON’s implementation. Currently, RACCOON carries out only consistency checks, and can be run online; its code is also publicly available. Besides, results of a comparison among RACCOON and other reasoners on the ORE 2014 and 2015 competition problems with ALC expressivity are shown and discussed.
ARCH-COMP17 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics
Authors: Althoff Matthias , Bak Stanley , Cattaruzza Dario , Chen Xin , Frehse Goran , Ray Rajarshi , Schupp Stefan
Published: January 2018

This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. In its first edition, seven tools have been applied to solve three different benchmark problems in the category for linear continuous dynamics (in alphabetical order): Axelerator, CORA, Flow*, HyDRA, Hylaa, SpaceEx, and XSpeed. The result is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results probably provide the most complete assessment of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.
High-level Hybrid Systems Analysis with Hypy
Authors: Bak Stanley , Bogomolov Sergiy , Schilling Christian
Published: January 2018

Hybrid systems play an important role in many application domains. A range of powerful analysis methods for this class of systems perform high-level analysis, where, iteratively, (1) a reachability computation is performed on a system model, (2) the result of the analysis is examined, and (3) the model is modified and the process repeats. For example, a well- known high-level analysis method is counter-example guided abstraction refinement (CEGAR), where, at each iteration, the model is refined based on the counter-example produced by the reachability computation.

In this paper, we present hypy, a python library which strives to ease the development of high-level analysis approaches. Hypy provides the necessary machinery to run a number of up-to-date hybrid systems analysis tools, parse their outputs, and modify the models. The modifications are performed using HyST, a source-to-source model transformation framework, which supports output formats including SpaceEx, Flow*, dReach, and HyCreate. HyST, however, does not run reachability tools nor interpret their output. The developed hypy library fills this gap, providing an extendable and flexible architecture which simplifies development of complex analysis strategies. We demonstrate its practical potential on three non-CEGAR case studies: abstraction for parameter identification, generation of pseudo-invariants to reduce reachability overapproximation error, and completely automatic tool parameter tuning for the Flow* reachability tool.
Logtk : A Logic ToolKit for Automated Reasoning and its Implementation
Authors: Cruanes Simon
Published: January 2018

We describe the design and implementation of Logtk, an OCaml library for writing automated reasoning tools that deal with (possibly typed) first-order logic. The library provides data structures and algorithms to represent terms, formulas, substitutions, perform unification, index terms, parse problems, as well as a few tools to demonstrate itsuse. It is the basis of a full-fledged superposition prover.
Almost structural completeness; an algebraic approach
Authors: Dzik Wojciech , Stronkowski Michał
Published: January 2018

The notion of structural completeness has received considerable attention for many years. A translating to algebra gives: a quasivariety is structurally complete if it is generated by its free algebras. It appears that many deductive systems (quasivarieties), like S5 or MVn fails structural completeness for a rather immaterial reason. Therefore the adjusted notion was introduced: almost structural completeness. We investigate almost structural completeness from an algebraic perspective and obtain a characterization of this notion for quasivarieties.
Modal Location-Resource-Process Logic for Access Control
Authors: Pym David
Published: January 2018

The logic MBI is a substructural modal logic of locations, resources, and processes that is closely related to both the bunched logic BI and Hennessy-Milner logic. MBI stands in a (slightly weak) Hennessy-Milner correspondence with the synchronous process calculus of located resources, LSCRP. Starting from motivations in large-scale systems modelling, I will introduce MBI and LSCRP, and explain how they can be used to address some theoretical and practical questions in access control.
The SMT Execution Service: Features, Fairness, and the Future
Authors: Deters Morgan
Published: January 2018

The SMT-Exec service is a benchmark repository, execution service, and competition infrastructure for the SMT community. Besides running the yearly competition and providing real-time (and also archival) results and analysis, SMT-Exec permits "private experiments" to be run year-round by researchers all over the world. These experiments are just like the yearly competition and run on the same computing cluster, but may be parameterized by users to run on benchmark and solver subsets of interest with a configurable timeout. Private solvers may be uploaded and tested against each other or against archival versions of competition solvers, and solvers and experiment results may be "published" so that they are publicly viewable. This talk describes SMT-Exec design highlights, challenges, growing pains, and current development plans for future versions of SMT-Exec.
Dialogues for proof search
Authors: Alama Jesse
Published: January 2018

Dialogue games are a two-player semantics for a variety of logics, including intuitionistic and classical logic. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. Can dialogue games be an effective foundation for proof search in intuitionistic logic (both first-order and propositional)? We announce Kuno, an automated theorem prover for intuitionistic first-order logic based on dialogue games.
A Comparison of Solvers for Propositional Dynamic Logic
Authors: Hustadt Ullrich , Schmidt Renate A.
Published: January 2018

Calculi for propositional dynamic logics have been investigated since the introduction of this logic in the late seventies. Only in recent years have practical procedures been suggested and implemented. In this paper, we compare three such systems, namely, the Tableau Workbench by Abate, Gore, and Widmann (2009), the pdlProver system by Gore and Widmann (2009), and the MLSolver system by Friedmann and Lange (2009).
Theorem Proving for Logic with Partial Functions Using Kleene Logic and Geometric Logic
Authors: De Nivelle Hans
Published: January 2018

We introduce a theorem proving strategy for Partial Classical Logic (PCL) that

is based on geometric logic. The strategy first translates PCL theories into sets of Kleene formulas. After that, the Kleene formulas are translated into 3-valued geometric logic. The resulting formulas can be refuted by an adaptation of

geometric resolution.

The translation to Kleene logic does not only open the way to theorem proving, but

it also sheds light on the relation between PCL, Kleene Logic, and classical logic.
Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers
Authors: Heule Marijn , Manthey Norbert , Philipp Tobias
Published: January 2018

As satisfiability (SAT) solver performance has improved, so has their complexity, which make it more likely that SAT solvers contain bugs. One important source of increased complexity is clause sharing in parallel SAT solvers. SAT solvers can emit a proof of unsatisfiability to gain confidence that the their results are correct. Such proofs must contain deletion information in order to check them efficiently. Computing deletion information is easy and cheap for parallel solvers without clause sharing, but tricky for parallel solvers with clause sharing.

We present a method to generate unsatisfiability proofs from clause sharing parallel SAT solvers. We show that the overhead of our method is small and that the produced proofs can be validated in a time similar to the solving (CPU) time. However, proofs produced by parallel solvers without clause sharing can be checked in a similar to the solving (wall-clock) time. This raises the question whether our method can be improved such that the checking time of proofs from parallel solvers without clause sharing is comparable to the time to check proofs from parallel solver with clause sharing.
Analysis of Portfolio-Style Parallel SAT Solving on Current Multi-Core Architectures
Authors: Aigner Martin , Biere Armin , Kirsch Christoph , Niemetz Aina , Preiner Mathias
Published: January 2018

Effectively parallelizing SAT solving is an open and

important issue. The current state-of-the-art is

based on parallel portfolios. This technique relies

on running multiple solvers on the same instance in

parallel. As soon one instance finishes the entire

run stops. Several succesful systems even use plain

parallel portfolio (PPP), where the individual solvers

do not exchange any information. This paper contains

a thorough experimental evaluation which shows that PPP

can improve wall-clock running time because memory access

is still local, respectively the memory system can hide

the latency of memory access. In particular, there does

not seem as much cache congestion as one might imagine.

We also present some limits on the scalibility of PPP.

Thus this paper gives one argument why PPP solvers are a

good fit for todays multi-core architectures.
A Sudoku-Solver for Large Puzzles using SAT
Authors: Pfeiffer Uwe , Karnagel Tomas , Scheffler Guido
Published: January 2018

n2 x n2 Sudoku puzzles can be straightforwardly encoded as SAT problems. However, solving such puzzles for large n requires a significant amount of optimization. We present some ideas for reducing the number of clauses, for improving the encoding, and for the selection of suitable SAT solvers.
On the Mathematical Boundaries of Communication with Zero-Capacity Quantum Channels
Authors: Gyongyosi Laszlo , Imre Sandor
Published: January 2018

In the first decade of the 21st century, many revolutionary properties of quantum channels were discovered. These phenomena are purely quantum mechanical and completely unimaginable in classical systems. Recently, the most important discovery in Quantum Information Theory was the possibility of transmitting quantum information over zero-capacity quantum channels. In this work we prove that the possibility of superactivation of quantum channel capacities is determined by the mathematical properties of the quantum relative entropy function.
Towards a Semantics of Unsatisfiability Proofs with Inprocessing
Authors: Philipp Tobias , Rebola-Pardo Adrián
Published: January 2018

Delete Resolution Asymmetric Tautology (DRAT) proofs have become a de facto standard to certify unsatisfiability results from SAT solvers with inprocessing. However, DRAT shows behaviors notably different from other proof systems: DRAT inferences are non- monotonic, and clauses that are not consequences of the premises can be derived. In this paper, we clarify some discrepancies on the notions of reverse unit propagation (RUP) clauses and asymmetric tautologies (AT), and furthermore develop the concept of resolution consequences. This allows us to present an intuitive explanation of RAT in terms of permissive definitions. We prove that a formula derived using RATs can be stratified into clause sets depending on which definitions they require, which give a strong invariant along RAT proofs. We furthermore study its interaction with clause deletion, characterizing DRAT derivability as satisfiability-preservation.
Critical Pair Analysis in Nominal Rewriting
Authors: Suzuki Takaki , Kikuchi Kentaro , Aoto Takahito , Toyama Yoshihito
Published: January 2018

Nominal rewriting (Fernández, Gabbay & Mackie, 2004;

Fernández & Gabbay, 2007) is a framework that extends

first-order term rewriting by a binding mechanism

based on the nominal approach (Gabbay & Pitts, 2002;

Pitts, 2003). In this paper, we investigate confluence

properties of nominal rewriting, following the study of

orthogonal systems in (Suzuki et al., 2015), but here

we treat systems in which overlaps of the rewrite rules

exist. First we present an example where choice of

bound variables (atoms) of rules affects joinability of

the induced critical pairs. Then we give a detailed

proof of the critical pair lemma, and illustrate some

of its applications including confluence results for

non-terminating systems.
Reconstructing Information Retrieved from Multiple Websites
Authors: Valero Héctor , Castillo Carlos , Silva Josep
Published: January 2018

This work presents a model for information retrieval from multiple webpages. This model does not need to pre-process, parser or label the webpages; and thus, it can work online and in real time. The model introduces two new techniques for visualization that allows us to automatically reconstruct a new webpage with the information retrieved. This page is structured taking into account the semantically related information. The technique has been implemented and the implementation is discussed focussing on the main problems that appear when the proposed algorithms are integrated into a commercial web browser.
Hybrid Automata Model of the Heart for Formal Verification of Pacemakers
Authors: Andalam Sidharta , Malik Avinash , Roop Partha , Trew Mark
Published: January 2018

A cardiac model of networked Hybrid Automata (HA) cells or nodes is potentially very useful for industry validation of pacemaker algorithms. Such a model replicates the electrical conduction system of the heart and the interaction with a pacemaker. The benchmark is a network of more than 100 HAs. It exhibits several key phenomena that are typical for hybrid systems and reachability analysis.
On modal components of the S4-logics
Authors: Muravitsky Alexei Y
Published: January 2018

We consider the representation of each extension of the modal logic S4 as sum of two components. The first component in such a representation is always included in Grzegorczyk logic and hence contains "modal resources" of the logic in question, while the second one uses essentially the resources of a corresponding intermediate logic. We prove some results towards the conjecture that every S4-logic has a representation with the least component of the first kind.
Implementing Polymorphism in Zenon
Authors: Bury Guillaume , Cauderlier Raphaël , Halmagrand Pierre
Published: January 2018

Extending first-order logic with ML-style polymorphism allows to define

generic axioms dealing with several sorts. Until recently, most

automated theorem provers relied on preprocess encodings into

mono/many-sorted logic to reason within such theories. In this paper, we

discuss the implementation of polymorphism into the

first-order tableau-based automated theorem prover Zenon. This

implementation leads to slightly modify some basic parts of the code,

from the representation of expressions to the proof-search algorithm.
Lebesgue Constants and Optimal Node Systems via Symbolic Computations
Authors: Vajda Robert
Published: January 2018

Polynomial interpolation is a classical method to approximate

continuous functions by polynomials. To measure the correctness of the

approximation, Lebesgue constants are introduced. For a given node system $X^{(n+1)}=\{x_1<\ldots<x_{n+1}\}\, (x_j\in [a,b])$, the Lebesgue function $\lambda_n(x)$ is the sum of the modulus of the Lagrange basis polynomials built on $X^{(n+1)}$. The Lebesgue constant $\Lambda_n$ assigned to the function $\lambda_n(x)$ is its maximum over $[a,b]$. The Lebesgue constant bounds the interpolation error, i.e., the interpolation polynomial is at most $(1+\Lambda_n)$ times worse then the best approximation.

The minimum of the $\Lambda_n$'s for fixed $n$ and interval $[a,b]$ is called the optimal Lebesgue constant $\Lambda_n^*$.

For specific interpolation node systems such as the equidistant system, numerical results for the Lebesgue constants $\Lambda_n$ and their asymptotic

behavior are known \cite{3,7}. However, to give explicit symbolic expression for the minimal Lebesgue constant $\Lambda_n^*$ is computationally difficult. In this work, motivated by Rack \cite{5,6}, we are interested for expressing the minimal

Lebesgue constants symbolically on $[-1,1]$ and we are also looking for the

characterization of the those node systems which realize the

minimal Lebesgue constants. We exploited the equioscillation property of the Lebesgue function \cite{4} and

used quantifier elimination and Groebner Basis as tools \cite{1,2}. Most of the computation is done in Mathematica \cite{8}.
Relevant logic and relation algebras
Authors: Kowalski Tomasz
Published: January 2018

In 2007, Maddux observed that certain classes of representable relation

algebras (RRAs) form sound semantics for some relevant logics. In particular,

(a) RRAs of transitive relations are sound for R, and (b) RRAs of transitive,

dense relations are sound for RM. He asked whether they were complete as

well. Later that year I proved a modest positive result in a similar direction,

namely that weakly associative relation algebras, a class (much) larger than

RRA, is sound and complete for positive relevant logic B. In 2008, Mikulas proved a

negative result: that RRAs of transitive relations are not complete for R.

His proof is indirect: he shows that the quasivariety of appropriate

reducts of transitive RRAs is not finitely based. Later Maddux re-established

the result in a more direct way. In 2010, Maddux proved a contrasting positive result: that transitive, dense RRAs are complete for RM. He found an embedding of Sugihara algebras into transitive, dense RRAs. I will show that if we give up the requirement of representability, the positive result holds for R as well. To be precise, the following theorem holds.

Theorem. Every normal subdirectly irreducible De Morgan monoid in the language

without Ackermann constant can be embedded into a square-increasing relation

algebra. Therefore, the variety of such algebras is sound and complete for R.
Extended Abstract: Getting Engaged
Authors: Thompson Simon
Published: January 2018

How do we engage with the artefacts that we build as software engineers or computer scientists?
Abduction for Learning Smart City Rules
Authors: Bjorner Nikolaj , Marinescu Maria-Cristina , Sagiv Mooly
Published: January 2018

We propose using abduction for inferring implicit rules for Smart City ontologies.

We show how we can use Z3 to extract candidate abducers from partial ontologies and leverage them in an iterative process of evolving an ontology by refining relations and restrictions, and populating relations.

Our starting point is a Smart City initiative of the city of Barcelona, where a substantial ontology is being developed to support processes such as city planning, social services, or improving the quality of the data concerning (for instance) legal entities, whose incompleteness may sometimes hide fraudulent behavior. In our scenario we are supporting semantic queries over heterogeneous and noisy data. The approach we develop would allow evolving ontologies in an iterative fashion as new relations and restrictions are discovered.
A Developer-oriented Hoare Logic
Authors: Gast Holger
Published: January 2018

We present a Hoare logic and verification system designed to be understandable by developers. We discuss both the underlying considerations on the design of the system, and the formal and technical background of the tools. We show that the goals have been achieved by typical examples.
Reasoning in the presence of inconsistency through Preferential ALC
Authors: Deane Graham , Broda Krysia , Russo Alessandra
Published: January 2018

This paper presents an inconsistency tolerant semantics for the Description Logic ALC called Preferential ALC (p-ALC). A p-ALC knowledge base is comprised of defeasible and non-defeasible axioms. The defeasible ABox and TBox are labelled with confidence weights that could reflect an axiom's provenance. Entailment is defined through the notion of preferred interpretations which minimise the total weight of the inconsistent axioms. We introduce a modified ALC tableau algorithm in which the open branches give rise to the preferred interpretations, and show that it can compute p-ALC entailment by refutation. The modified algorithm is implemented as an incremental answer set program (ASP) that exploits optimisation to capture preferred interpretations of p-ALC.
Acceleration For Presburger Petri Nets
Authors: Leroux Jerome
Published: January 2018

The reachability problem for Petri nets is a central problem of net theory. The problem is known to be decidable by inductive invariants definable in the Presburger arithmetic. When the reachability set is definable in the Presburger arithmetic, the existence of such an inductive invariant is immediate. However, in this case, the computation of a Presburger formula denoting the reachability set is an open problem. Recently this problem got closed by proving that if the reachability set of a Petri net is definable in the Presburger arithmetic, then the Petri net is flatable, i.e. its reachability set can be obtained by runs labeled by words in a bounded language. As a direct consequence, classical algorithms based on acceleration techniques effectively compute a formula in the Presburger arithmetic denoting the reachability set.
Testbed for Model-based Verification of Cyber-physical Production Systems
Authors: Budnik Christof J. , Eckl Sebastian , Gario Marco
Published: January 2018

Cyber-physical production systems (CPPS) build a network of industrial automation components and systems to enable individualized products at mass production costs. Failures or vulnerabilities in CPPS can be life threatening and can cause physical damage while hiding the effects from monitors. Thus, software verification and validation methods need to analyze the dynamics and behavior of CPPS. In this work, we present a hybrid testbed used in Siemens Corporate Technology. The testbed combines a physical CPPS together with its virtual simulated counterpart, allowing us to verify the system using runtime monitoring, model-based testing, simulation and formal techniques.
Cognition, Concurrency Theory and Reverberations in the Brain: in Search of a Calculus of Communicating (Recurrent) Neural Systems
Authors: Bowman Howard , Su Li
Published: January 2018

We consider whether techniques from concurrency theory can be applied in the area of Cognitive Neuroscience. We focus on two potential applications. The first of these explores structural decomposition, which is effectively assumed by the localisation of function metaphor that so dominates current Cognitive Neuroscience. We take concurrency theory methods, especially Process Calculi, as canonical illustrations of system description notations that support structural decomposition and, in particular, encapsulation of behaviour. We argue that carrying these behavioural and notational properties over to the Cognitive Neuroscience setting is difficult, since neural networks (the modelling method of choice) are not naturally encapsulable. Our second application presents work on verifying stability properties of neural network learning algorithms using model checking. We thereby present evidence that a particular learning algorithm, the Generalised Recirculation algorithm, exhibits an especially severe form of instability, whereby it forgets what it has learnt, while continuing to be trained on the same pattern set.
An Algebra of Combined Constraint Solving
Authors: Ternovska Eugenia
Published: January 2018

The paper describes a project aiming at developing formal foundations

of combined multi-language constraint solving in the form of an algebra of modular systems.

The basis for integration of different formalisms is the classic model theory.

Each atomic module is a class of structures.

It can be given, e.g., by a set of constraints in a constraint formalism

that has an associated solver.

Atomic modules are combined using a small number of algebraic operations.

The algebra simultaneously resembles Codd's relational algebra, (but is defined

on classes of structures instead of relational tables), and process

algebras originated in the work of Milner and Hoare.

The goal of this paper is to establish and justify

the main notions and research directions,

make definitions precise.

We explain several results, but do not give proofs.

The proofs will appear in several forthcoming papers.

We keep this paper as a project description paper to discuss the overall project,

to establish and bridge individual directions.
Determining automatically compass and straightedge unconstructibility in triangles
Authors: Mathis Pascal , Schreck Pascal
Published: January 2018

In many areas, some geometry problems can not be solved using only geometry and are treated by the means of algebraic tools. However, geometric properties can be still employed to simplify the system of equations. This allows either to speed up the treatment or, more radically, to make the treatment possible. In this article we illustrate this approach with a family of toy examples. In all these problems the goal it is to determine if there is a compass-and-straightedge construction of the three vertices of a triangle knowing only three located points of this triangle. Algebraic tools, basically Galois theory, are needed to answer the question. But in many cases a geometric reasoning phase is required to provide a polynomial algebraic system that algebraic softwares can address within a acceptable time despite the exponential complexity of the underlying algorithms.
Abstract Domains for Bit-Level Machine Integer and Floating-point Operations
Authors: Miné Antoine
Published: January 2018

We present a few lightweight numeric abstract domains to analyze C programs that

exploit the binary representation of numbers in computers, for instance to

perform ``compute-through-overflow'' on machine integers, or to directly

manipulate the exponent and mantissa of floating-point numbers.

On integers, we propose an extension of intervals with a modular component,

as well as a bitfield domain.

On floating-point numbers, we propose a predicate domain to match, infer,

and propagate selected expression patterns.

These domains are simple, efficient, and extensible.

We have included them into the Astree and AstreeA static analyzers to

supplement existing domains. Experimental results show that they can improve

the analysis precision at a reasonable cost.
Coq without Type Casts: A Complete Proof of Coq Modulo Theory
Authors: Jouannaud Jean-Pierre , Strub Pierre-Yves
Published: January 2018

Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality lead to undecidable type-checking, a good trade-off is to extend intensional equality with a decidable first-order theory T, as done in CoqMT, which uses matching modulo T for the weak and strong elimination rules, we call these rules T-elimination. So far, type-checking in CoqMT is known to be decidable in presence of a cumulative hierarchy of universes and weak T-elimination. Further, it has been shown by Wang with a formal proof in Coq that consistency is preserved in presence of weak and strong elimination rules, which actually implies consistency in presence of weak and strong T-elimination rules since T is already present in the conversion rule of the calculus.

We justify here CoqMT’s type-checking algorithm by showing strong normalization as well as the Church-Rosser property of β-reductions augmented with CoqMT’s weak and strong T -elimination rules. This therefore concludes successfully the meta-theoretical study of CoqMT.