bluuebunny/crossref_metadata_2025 huggingface dataset:
The Glory of the Past and Geometrical Concurrency
Authors: Prisacariu Cristian
Published: January 2018

This paper contributes to the general understanding of the "geometrical model of concurrency" that was named higher dimensional automata (HDAs) by Pratt and van Glabbeek. In particular we provide some understanding of the modal logics for such models and their expressive power in terms of the bisimulation that can be captured.

The geometric model of concurrency is interesting from two main reasons: its generality and expressiveness, and the natural way in which autoconcurrency and action refinement are captured.

Logics for this model, though, are not well investigated, where a simple, yet adequate, modal logic over HDAs was only recently introduced.

As this modal logic, with two existential modalities, "during" and "after", captures only split bisimulation, which is rather low in the spectrum of van Glabbeek and Vaandrager, the immediate question was what small extension of this logic could capture the more fine-grained hereditary history preserving bisimulation (hh)?

In response, the work in this paper provides several insights. One is the fact that the geometrical aspect of HDAs makes it possible to use for capturing the hh-bisimulation, a standard modal logic that does not employ event variables, opposed to the two logics (over less expressive models) that we compare with. The logic that we investigate here uses standard backward-looking modalities (i.e., past modalities) and extends the previously introduced logic (called HDML) that had only forward, action-labelled, modalities.

Since the direct proofs are rather intricate, we try to understand better the above issues by introducing a related model that we call ST-configuration structures, which extend the configuration structures of van Glabbeek and Plotkin. We relate this model to HDAs, and redefine and prove the earlier results in the light of this new model. These offer a different view on why the past modalities and geometrical concurrency capture the hereditary history preserving bisimulation.

Additional correlating insights are also gained.
Real Analysis for Complex Systems
Authors: Platzer Andrè
Published: January 2018

Formal verification techniques are used routinely in finite-state digital circuits. Theorem proving is also used successfully for infinite-state discrete systems. But many safety-critical computers are actually embedded in physical systems. Hybrid systems model complex physical systems as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. They arise frequently in many application domains, including aviation, automotive, railway, and robotics. There is a well-understood theory for proving programs. But what about complex physical systems? How can we prove that a hybrid system works as expected, e.g., an aircraft does not crash into another one?

This talk illustrates the complexities and pitfalls of hybrid systems verification. It describes a theoretical and practical foundation for deductive verification of hybrid systems called differential dynamic logic. The proof calculus for this logic is interesting from a theoretical perspective, because it is a complete axiomatization of hybrid systems relative to differential equations. The approach is of considerable practical interest too. Its implementation in the theorem prover KeYmaera has been used successfully to verify collision avoidance properties in the European Train Control System and air traffic control systems. The number of dimensions and nonlinearities in they hybrid dynamics of these systems is surprisingly tricky such that they are still out of scope for other verification tools.
Beating the Productivity Checker Using Embedded Languages
Authors: Danielsson Nils Anders
Published: January 2018

Some total languages, like Agda and Coq, allow the use of guarded corecursion to construct infinite values and proofs. Guarded corecursion is a form of recursion in which arbitrary recursive calls are allowed, as long as they are guarded by a coinductive constructor. Guardedness ensures that programs are productive, i.e. that every finite prefix of an infinite value can be computed in finite time. However, many productive programs are not guarded, and it can be nontrivial to put them in guarded form.

This paper gives a method for turning a productive program into a guarded program. The method amounts to defining a problem-specific language as a data type, writing the program in the problem-specific language, and writing a guarded interpreter for this language.
Pandora's Box
Authors: Middelkoop Ronald , Huizing Cornelis , Kuiper Ruurd , Luit Erik J.
Published: January 2018

An algebraic specification is viewed as a black box that rewrites input to a ``most basic'' canonical form. We argue that a canonical form should be given for each specific specification, to prevent ``cheating'' in the implementation. Furthermore, we argue that the definition of the canonical form may sometimes require semantic rather than syntactic information.

To relate an OO implementation to a specification requires opening the black box to some extent; we assess the choices to be made here.
Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus
Authors: Fiorino Guido
Published: January 2018

We present a procedure to decide propositional Dummett logic. Such a procedure relies on a tableau calculus with a multiple premise rule and optimizations. The resulting implementation outperforms the state of the art graph-based procedure.
Laterally complete and projective hulls of semilinear residuated lattices
Authors: Gil-Férez José , Ledda Antonio , Tsinakis Constantine
Published: January 2018

The existence of lateral completions of ℓ-groups is an old problem that was first solved, for conditionally complete vector lattices, by Nakano. The existence and uniqueness of lateral completions of representable ℓ-groups was first obtained as a consequence of the orthocompletions of Bernau, and later the proofs were simplified by Conrad, who also proved the existence and uniqueness of lateral completions of ℓ-groups with zero radical. Finally, Bernau solved the problem for ℓ-groups in general.

In this work, we address the problem of the existence and uniqueness of lateral, projectable, and strongly projectable completions of residuated lattices. In particular, we push the methods of Conrad through to the case of the representable GMV-algebras.

The leading idea is to construct, for any given semilinear residuated lattice, an orthocomplete extension such that the former is dense in the latter. This extension is obtained as the direct limit of a family of residuated lattices that are constructed using maximal partitions of the algebra of polars of the original residuated lattice.

In order to complete the proof we still need another hypothesis, which is an abstraction of the condition of double negation in which commutativity and integrality have been dropped, and determines the wide class of Generalized MV-algebras. This, together with the density, allows us to obtain the completions of the given residuated lattice.
Satisfiability Checking and Query Answering for Large Ontologies
Authors: Weidenbach Christoph , Wischnewski Patrick
Published: January 2018

In this paper we develop a sound, complete and terminating superposition calculus

plus a query answering calculus for the BSH-Y2 fragment of the

Bernays-Schoenfinkel Horn class of first-order logic.

BSH-Y2 can be used to represent expressive ontologies.

In addition to checking consistency, our calculus supports query answering

for queries with arbitrary quantifier alternations.

Experiments on BSH-Y2 (fragments) of several large ontologies show that our

approach advances the state of the art.
Bunched Hypersequent Calculi for Distributive Substructural Logics
Authors: Ciabattoni Agata , Ramanayake Revantha
Published: January 2018

We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure. A general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions is then proved. We adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus DFLe and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.
Bit-size reduction of triangular sets in two and three variables
Authors: Yamashita Tetsuro , Dahan Xavier
Published: January 2018

At ISSAC 2004, Schost and D.

introduced a transformation of triangular lexicographic Groebner bases

generating a radical ideal of dimension zero,

which reduces significantly the bit-size of coefficients.

The case where the triangular lexicographic Groebner basis does not generate a radical ideal

is far more complicated. This work treats the case of n=2 variables, and

in some extent the case of n=3 variables.

It resorts to an extra operation, the squarefree factorization;

nevertheless this operation has low complexity cost.

But as soon as n>2 variables a lack of simple and efficient gcd-like operation

over non-reduced rings prevents to undertake meaningful algorithmic considerations.

An implementation in Maple for the case n=2 confirms the expected

reduction of the expected size coefficients.
Deep Proof Search in MELL
Authors: Kahramanogullari Ozan
Published: January 2018

The deep inference presentation of multiplicative exponential linear logic (MELL) benefits from a rich combinatoric analysis with many more proofs in comparison to its sequent calculus presentation. In the deep inference setting, all the sequent calculus proofs are preserved. Moreover, many other proofs become available, and some of these proofs are much shorter. However, proof search in deep inference is subject to a greater nondeterminism, and this nondeterminism constitutes a bottleneck for applications. To this end, we address the problem of reducing nondeterminism in MELL by refining and extending our technique that has been previously applied to multiplicative linear logic and classical logic. We show that, besides the nondeterminism in commutative contexts, the nondeterminism in exponential contexts can be reduced in a proof theoretically clean manner. The method conserves the exponential speed-up in proof construction due to deep inference, exemplified by Statman tautologies. We validate the improvement in accessing the shorter proofs by experiments with our implementations.
Priestley duality for (modal) N4-lattices
Authors: Jansana Ramon , Rivieccio Umberto
Published: January 2018

N4-lattices are the algebraic semantics of paraconsistent Nelson logic, which was introduced as an inconsistency-tolerant counterpart of the better-known logic of Nelson. Paraconsistent Nelson logic combines interesting features of intuitionistic, classical and many-valued logics (e.g., Belnap-Dunn four-valued logic); recent work has shown that it can also be seen as one member of the wide family of substructural logics.

The work we present here is a contribution towards a better topological understanding of the algebraic counterpart of paraconsistent Nelson logic, namely a variety of involutive lattices called N4-lattices.
Secure Communication over Zero-Private Capacity Quantum Channels
Authors: Gyongyosi Laszlo , Imre Sandor
Published: January 2018

In this work a new phenomenon called polaractivation is introduced. Polaractivation is based on quantum polar encoding and the result is similar to the superactivation effect — positive capacity can be achieved with zero-capacity quantum channels. However, polaractivation has many advantages over the superactivation: it is limited neither by any preliminary conditions on the quantum channel nor on the maps of other channels involved in the joint channel structure. We prove that the polaractivation works for arbitrary zero-private capacity quantum channels and we demonstrate, that the symmetric private classical capacity of arbitrary zero-private capacity quantum channels is polaractive.
Invariants and Robustness of BIP Models
Authors: Blech Jan Olaf , Nguyen Thanh-Hung , Perin Michael
Published: January 2018

In this paper we present on-going work addressing the problem of automatically generating realistic and guaranteed correct invariants. Since invariant generation mechanisms are error-prone, after the computation of invariants by a verification tool, we formally prove that the generated invariants are indeed invariants of the considered systems using a higher-order theorem prover and automated techniques. We regard invariants for BIP models. BIP (behavior, interaction, priority) is a language for specifying asynchronous component based systems. Proving that an invariant holds often requires an induction on possible system execution traces. For this reason, apart from generating invariants that precisely capture a system’s behavior, inductiveness of invariants is an important goal. We establish a notion of robust BIP models. These can be automatically constructed from our original non-robust BIP models and over-approximate their behavior. We motivate that invariants of robust BIP models capture the behavior of systems in a more natural way than invariants of corresponding non-robust BIP models. Robust BIP models take imprecision due to values delivered by sensors into account. Invariants of robust BIP models tend to be inductive and are also invariants of the original non-robust BIP model. Therefore they may be used by our verification tools and it is easy to show their correctness in a higher-order theorem prover. The presented work is developed to verify the results of a deadlock-checking tool for embedded systems after their computations. Therewith, we gain confidence in the provided analysis results.
Legal Information Retrieval Using Topic Clustering and Neural Networks
Authors: Nanda Rohan , Kolawole John Adebayo , Di Caro Luigi , Boella Guido , Robaldo Livio
Published: January 2018

This paper presents a description about our adopted approach for the information retrieval and textual entailment tasks of the COLIEE 2017 competition. We address the information retrieval task by implementing a partial string matching and a topic clustering method. For the textual entailment task, we propose a Long Short-Term Memory (LSTM) - Convolutional Neural Network (CNN) model which utilizes word embeddings trained on the Google News vectors. We evaluated our approach for both tasks on the COLIEE 2017 dataset. The results demonstrate that the topic clustering method outperformed the partial string matching method in the information retrieval task. The performance of LSTM-CNN model was competitive with other textual entailment systems.
Recent Advances in Unification for the EL Family
Authors: Baader Franz , Borgwardt Stefan , Morawska Barbara
Published: January 2018

Unification in description logics (DLs) has been proposed as a means to detect redundancies in ontologies. The DL EL, even though quite inexpressive, can be used to formulate large medical ontologies like SNOMED CT. Previously, several unification algorithms for EL were developed that can only deal with acyclic terminologies. In this paper, we give an overview over our recent efforts to generalize these algorithms to allow for general concept inclusions, transitive roles, and role hierarchies. For our new algorithms to be complete, the ontology needs to satisfy a certain cycle restriction.
Trie Based Subsumption and Improving the pi-Trie Algorithm
Authors: Matusiewicz Andrew , Murray Neil , Rosenthal Erik
Published: January 2018

An algorithm that stores the prime implicates of a logical formula in a trie was developed in [Matusiewicz et.al. 2009]. In this paper, an improved version of that pi-trie algorithm is presented. It achieves its speedup primarily by significantly decreasing subsumption testing. Preliminary experiments indicate the new algorithm to be substantially faster and the trie based subsumption tests to be considerably more efficient than the clause by clause approach originally employed.
Trust, Belief and Honesty
Authors: Pearce David , Uridia Levan
Published: January 2018

We study two modal logics of trust that interconnect the trust modality with the individual belief modalities of agents. One logic includes an axiom stating that if agent i trusts agent j with respect to a statement p then i believes that j does not disbelieve p. In the second logic, if i trusts j concerning p then i believes that j believes p. These extensions of the logic of trust help to solve some unintuitive consequences that arise when the semantics of trust and belief are independent. As a main technical result we prove the soundness and completeness of these logics.
An Autonomous Vehicle Control Stack
Authors: Rodionova Alena , O'Kelly Matthew , Abbas Houssam , Pacelli Vincent , Mangharam Rahul
Published: January 2018

This benchmark presents an implementation of a standard control stack for an Autonomous Vehicle (AV). The control stack is made up of a behavioral planner (providing waypoints for the AV to visit in sequence), a trajectory planner (which computes smooth trajectory that the AV should follow to go between waypoints) and a trajectory tracker (which actuates the AV to make it follow the planned trajectory as closely as possible). The behavioral planner is purposefully simple, while the trajectory planner is a a high-fidelity approximation of a planner that was tested on a real Prius, and the tracker was validated by others in previous work on a real Cadillac SRX. The interest of this benchmark is that it includes all three components, rather than one AV control subsystem (such as only adaptive cruise control or only a lane-keeper), and the planners are significantly more realistic than most existing benchmarks or models. It can be used as a baseline AV system for verification and testing tools, which must be able to handle at least the complexity of this controller. This includes simple choices made by the behavioral planner when the current waypoint cannot be reached, discrete and continuous nonlinear optimizations solved by the trajectory planner, and nonlinear ODEs solved by the trajectory tracker. The bench- mark comes with three road topologies: a free space with obstacles, a curved road, and a roundabout.
Algorithmic correspondence for intuitionistic modal mu-calculus, Part 2
Authors: Conradie Willem , Fomatati Yves , Palmigiano Alessandra , Sourabh Sumit
Published: January 2018

Sahlqvist-style correspondence results remain a perennial theme and an active topic of research within modal logic. Recently there has been interest in extending classical results in this area to the modal mu-calculus. We show how the `calculus of correspondence' and the ALBA algorithm (Conradie and Palmigiano, 2012) can be extended to the intuitionistic mu-calculus, and be used to derive FO+LFP frame correspondents for formulas of that logic. We define the class of recursive mu-inequalities, which we compare it with related classes in the literature including the Sahlqvist mu-formulas of van Benthem, Bezhanishvili and Hodkinson. We show that the ALBA algorithm succeeds in reducing every recursive mu-inequality, and hence that every recursive mu-inequality has a frame correspondent in FO+LFP.
Machine Learner for Automated Reasoning 0.4 and 0.5
Authors: Kaliszyk Cezary , Urban Josef , Vyskocil Jiri
Published: January 2018

Machine Learner for Automated Reasoning (MaLARea) is a learning and

reasoning system for proving in large formal libraries where

thousands of theorems are available when attacking a new

conjecture, and a large number of related problems and proofs can be used to

learn specific theorem-proving knowledge. The last version of the

system has by a large margin won the 2013 CASC LTB competition. This

paper describes the motivation behind the methods used in MaLARea,

discusses the general approach and the issues arising in evaluation

of such system, and describes the Mizar@Turing100 and CASC'24

versions of MaLARea.
Distributed Autonomous Systems
Authors: Tran Hoang-Dung , Nguyen Luan Viet , Xiang Weiming , Johnson Taylor T.
Published: January 2018

This benchmark suite consists of a number of examples of autonomous multi-agent systems where the agent number ranges from two to ten. The benchmarks are derived from the field of position-based formation control in autonomous robotics and vehicles. Their models are given as network of hybrid automata in the SpaceEx XML model format and can be transformed to other verification tools model formats using HyST, a model trans- formation tool. Safety of a small benchmark with two agents is analyzed using SpaceEx.
A Logic for Verifying Metric Temporal Properties in Distributed Hybrid Systems
Authors: Hou Ping , Chen Yifei
Published: January 2018

We introduce a logic for specifying and verifying metric temporal properties of distributed hybrid systems that combines quantified differential dynamic logic (QdL) for reasoning about the possible behavior of distributed hybrid systems with metric temporal logic (MTL) for reasoning about the metric temporal behavior during their operation. For our combined logic, we generalize the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of QdL for distributed hybrid systems. On this basis, we provide a modular verification calculus that reduces correctness of metric temporal behavior of distributed hybrid systems to generic temporal reasoning and then non-temporal reasoning, and prove that we obtain a complete axiomatization relative to the non-temporal base logic QdL.
A New Proof of P-time Completeness of Linear Lambda Calculus
Authors: Matsuoka Satoshi
Published: January 2018

We give a new proof of P-time completeness of

the Linear Lambda Calculus, which was originally given by H. Mairson in 2003.

Our proof uses an essentially different Boolean type from the type that Mairson used.

Moreover the correctness of our proof can be machined-checked using an implementation of Standard ML.
BDD-based automated reasoning in propositional non-classical logics: progress report
Authors: Gore Rajeev , Thomson Jimmy
Published: January 2018

Recent work has shown that a technique using Binary Decision Diagrams (BDDs) to decide CTL and Int gives promising results. Based on this we explore how the method can be extended to other non-classical logics. In particular, we describe a putative method for deciding the modal mu-calculus using BDDs.
Symbolic WS1S
Authors: D'Antoni Loris , Veanes Margus
Published: January 2018

We extend weak monadic second-order logic of one successor (WS1S) to symbolic alphabets by

allowing character predicates to range over decidable first order theories and not just finite alphabets.

We call this extension symbolic WS1S (s-WS1S). We then propose two decision procedures for such a

logic: 1) we use symbolic automata to extend the classic reduction from WS1S to finite automata to

our symbolic logic setting; 2) we show that every s-WS1S formula can be reduced to a WS1S formula

that preserves satisfiability, at the price of an exponential blow-up.
Computing with Metabolic Machines
Authors: Angione Claudio , Carapezza Giovanni , Costanza Jole , Lio Pietro , Nicosia Giuseppe
Published: January 2018

If Turing were a first-year graduate student interested in computers,

he would probably migrate into the field of computational biology. During his studies, he presented

a work about a mathematical and computational model of the morphogenesis process, in which chemical substances

react together. Moreover, a protein can be thought of as a computational element, i.e. a processing unit, able to

transform an input into an output signal. Thus, in a biochemical pathway, an enzyme reads the amount of reactants (substrates)

and converts them in products. In this work, we consider the biochemical pathway in unicellular organisms (e.g. bacteria) as a living computer, and we are able to program it in order to obtain desired outputs.

The genome sequence is thought of as an executable code specified by a set of commands in a sort of ad-hoc low-level programming language. Each combination of genes is coded as a string of bits $y \in \left \{ 0 , 1 \right \}^L$, each of which represents a gene set. By turning off a gene set, we turn off the chemical reaction associated with it. Through an optimal executable code stored in the ``memory'' of bacteria, we are able to simultaneously maximise the concentration of two or more metabolites of interest.

Finally, we use the Robustness Analysis and a new Sensitivity Analysis method to investigate both the fragility of the computation carried out by bacteria and the most important entities in the mathematical relations used to model them.
Alternating Turing machines and the analytical hierarchy
Authors: Leivant Daniel
Published: January 2018

We use notions originating in Computational Complexity to provide insight into the analogies between computational complexity and Higher Recursion Theory. We consider alternating Turing machines, but with a modified, global, definition of acceptance. We show that a language is accepted by such a machine iff it is Pi-1-1. Moreover, total alternating machines, which either accept or reject each input, accept precisely the hyper-arithmetical (Delta-1-1) languages. Also, bounding the permissible number of alternations we obtain a characterization of the levels of the arithmetical hierarchy.

.

The novelty of these characterizations lies primarily in the use of finite computing devices, with finitary, discrete, computation steps. We thereby elucidate the correspondence between the polynomial-time and the arithmetical hierarchies, as well as that between the computably-enumerable, the inductive (Pi-1-1), and the PSpace languages.
Razor: Provenance and Exploration in Model-Finding
Authors: Saghafi Salman , Dougherty Daniel
Published: January 2018

Razor is a model-finder for first-order theories presented

geometric form; geometric logic is a variant of first-order logic

that focuses on ``observable'' properties. An important guiding

principle of Razor is that it be accessible to users who are

not necessarily expert in formal methods; application areas

include software design, analysis of security protocols and

policies, and configuration management.

A core functionality of the tool is that it supports

exploration of the space of models of a given input theory,

as well as presentation of provenance information about the

elements and facts of a model. The crucial mathematical tool is

the ordering relation on models determined by homomorphism, and

Razor prefers models that are minimal with respect to this

homomorphism-ordering.
Conditional Independence in Categories
Authors: Simpson Alex
Published: January 2018

In this talk I shall discuss a general category-theoretic structure for modelling conditional independence. The standard notion of conditional independence in probability theory provides a motivating example. But other rather different examples arise in many contexts: computability theory, nominal sets (used to model `names' in computer science), separation logic (used to reason about heap memory in computer science), and others.

Category-theoretic structure common to these examples can be axiomatized by the notion of a category with local independent products, which combines fibrational and symmetric monoidal structure in a somewhat particular way. In the talk I shall expound this notion, and I shall present several illustrative examples of such structure. If time permits, I may also describe some curious connections with topos theory.
On the modal logic of the iterated Cantor derivative and finitary operations on topological spaces
Authors: Saveliev Denis I.
Published: January 2018

We consider propositional language endowed with three families of modal operators:

operators of the first type are interpreted by iterations of the Cantor derivative, operators of the second and the third types are interpreted by the image and the preimage of finitary operations on a topological space. We describe logics in this language that are sound and complete w.r.t. operations of a certain kind: injective, continuous, open, closed, continuous and discrete, closed of finite rank, separately continuous and separately discrete, etc. These results are based on our recent work "On interactions of the Cantor derivative and images of finitary maps between topological spaces" (2012, submitted to Topology and its Applications).
Transforming Undecidable Synthesis Problems into Decidable Problems
Authors: Finkbeiner Bernd
Published: January 2018

Synthesis holds the promise to revolutionize the development of

complex systems by automating the translation from specifications to

implementations. Synthesis algorithms are based on the same level of

mathematical rigor as verification algorithms but can be applied at

earlier development stages, when only parts of the design are

available. Given a formal specification of the desired system

properties, for example in a temporal logic, we determine if the

partial design can be completed into a full design that satisfies the

properties.

For general distributed systems, the synthesis problem is undecidable.

However, there has been a sequence of discoveries where the

decidability was established for specific system architectures, such

as pipelines and rings, or other restrictions on the problem, such as

local specifications. Encouraged by these findings, new specification

languages like Coordination Logic aim for a uniform treatment of the

synthesis problem.

In this talk, I will review several techniques that transform

undecidable synthesis problems into decidable problems.
Specification Inference and Invariant Generation: A Machine Learning Perspective
Authors: Nori Aditya
Published: January 2018

Computing good specification and invariants is key to effective

and efficient program verification. In this talk, I will describe

our experiences in using machine learning techniques (Bayesian

inference, SVMs) for computing specifications and invariants

useful for program verification. The first project Merlin uses

Bayesian inference in order to automatically infer security

specifications of programs. A novel feature of Merlin is that it

can infer specifications even when the code under analysis gives

rise to conflicting constraints, a situation that typically

occurs when there are bugs. We have used Merlin to infer security

specifications of 10 large business critical web

applications. Furthermore, we show that these specifications can

be used to detect new information flow security vulnerabilities

in these applications.

In the second project Interpol, we show how interpolants can be

viewed as classifiers in supervised machine learning. This view

has several advantages: First, we are able to use off-the-shelf

classification techniques, in particular support vector

machines (SVMs), for interpolation. Second, we show that SVMs can

find relevant predicates for a number of benchmarks. Since

classification algorithms are predictive, the interpolants

computed via classification are likely to be relevant predicates

or invariants. Finally, the machine learning view also enables us

to handle superficial non-linearities. Even if the underlying

problem structure is linear, the symbolic constraints can give an

impression that we are solving a non-linear problem. Since

learning algorithms try to mine the underlying structure

directly, we can discover the linear structure for such

problems. We demonstrate the feasibility of Interpol via

experiments over benchmarks from various papers on program

verification.
Exploiting parallelism in the ME calculus
Authors: Liang Tianyi , Tinelli Cesare
Published: January 2018

We present some parallelization techniques for the Model Evolution (ME) calculus,

an instantiation-based calculus that lifts the DPLL procedure

to first-order clause logic.

Specifically, we consider a restriction of ME to the EPR fragment

of clause logic for which the calculus is a decision procedure.

The main operations in ME's proof procedures, namely clause instantiation

and candidate literal generation, offer opportunities for MapReduce-style

parallelization.

This term/clause-level parallelization is largely orthogonal to the sort

of search-level parallelization performed by portfolio approaches.

We describe a hybrid parallel proof procedure for the restricted calculus

that exploits parallelism at both levels to synergistic effect.

The calculus and the proof procedure have been implemented in

a new solver for EPR formulas.

Our initial experimental results show that our term/clause-level parallelization

alone is effective in reducing runtime and can be combined

with a portfolio-based approach to maximize performance.
Learning Importance of Preferences
Authors: Zhu Ying , Truszczynski Mirek
Published: January 2018

We study the problem of learning the importance of preferences in preference profiles in two important cases: when individual preferences are aggregated by the ranked Pareto rule, and when they are aggregated by positional scoring rules. For the ranked Pareto rule, we provide a polynomial-time algorithm that finds a ranking of preferences such that the ranked profile correctly decides all the examples, whenever such a ranking exists. We also show that the problem to learn a ranking maximizing the number of correctly decided examples (also under the ranked Pareto rule) is NP-hard. We obtain similar results for the case of weighted profiles when positional scoring rules are used for aggregation.
ARCH-COMP17 Category Report: Continuous Systems with Nonlinear Dynamics
Authors: Chen Xin , Althoff Matthias , Immler Fabian
Published: January 2018

We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2017. This year, three tools CORA, Flow* and Isabelle/HOL (in alphabetic order) participated. They are applied to solve the reachability analysis problems on three benchmarks which have 2, 7 and 12 variables respectively. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools. Besides, the computational settings presented here provide a guide to use the tools although they might not be optimal.
The Potential of Interference-Based Proof Systems
Authors: Heule Marijn , Kiesl Benjamin
Published: January 2018

In our extended abstract, we try to motivate researchers to investigate the potential of proof systems that modify a given set of formulas (e.g., a set of clauses in propositional logic) in a way that preserves satisfiability but not necessarily logical equivalence. We call such modifications interferences, because they

can change the models of a given set of formulas.
Coproducts of Distributive Lattice based Algebras
Authors: Cabrer Leonardo Manuel , Priestley Hilary
Published: January 2018

The analysis of coproducts in varieties of algebras has generally been variety-specific, relying on tools tailored to particular classes of algebras. A recurring theme, however, is the use of a categorical duality. Among the dualities and topological representations in the literature, natural dualities are particularly well behaved with respect to coproduct. Since (multisorted) natural dualities are based on hom-functors, they send coproducts into cartesian products.

We carry out a systematic study of coproducts for finitely generated quasivarieties A that admit a (term) reduct in the variety D of bounded distributive lattices.
Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain
Authors: Gao Yang , Fränzle Martin
Published: January 2018

Stochastic Satisfiability Modulo Theories (SSMT) is a quantitative exten-

sion of classical Satisfiability Modulo Theories (SMT) inspired by stochastic

logics. It extends SMT by the usual as well as randomized quantifiers, fa-

cilitating capture of stochastic game properties in the logic, like reachability

analysis of hybrid-state Markov decision processes. Solving for SSMT for-

mulae with quantification over finite and thus discrete domain has been ad-

dressed by Tino Teige et al. In our work, we extend their work to SSMT

over continuous quantifier domains (CSSMT) in order to enable capture of,

e.g., continuous disturbances and uncertainty in hybrid systems. We extend

the semantics of SSMT and introduce a corresponding solving procedure. A

discussion regarding to reachability analysis is given to demonstrate applica-

bility of our framework to reachability problems in hybrid systems.
Verifying Properties of an Electro-Mechanical Braking System
Authors: Strathmann Thomas , Oehlerking Jens
Published: January 2018

In this experience report, we apply the hybrid verification tools

iSAT-ODE, Flow*, and S-TaLiRo to a case study consisting of an experimental

electro-mechanical braking system. Starting from a Simulink closed-loop

model, we describe the derivation of hybrid automaton models for plant

and controller and give verifcation results for the different tools.
Properties of Constrained Generalization Algorithms
Authors: Boy de La Tour Thierry
Published: January 2018

Two non deterministic algorithms for generalizing a solution of a constraint expressed in second order typed lambda-calculus are presented. One algorithm derives from the proof of completeness of the higher order unification rules by D. C. Jensen and T. Pietrzykowski, the other is abstracted from an algorithm by N. Peltier and the author for generalizing proofs. A framework is developed in which such constrained generalization algorithms can be designed, allowing a uniform presentation for the two algorithms. Their relative strength at generalization is then analyzed through some properties of interest: their behaviour on valid and first order constraints, or whether they may be iterated or composed.
Defining the meaning of TPTP formatted proofs
Authors: Blanco Roberto , Libal Tomer , Miller Dale
Published: January 2018

The TPTP library is one of the leading problem libraries in the automated theorem proving community. Along the years, support was added for problems beyond those in first-order clausal form. Another addition was the augmentation of the language to support proofs outputted from theorem provers and the maintenance of a proof library, called TSTP. In this paper we propose another augmentation of the language for the support of the semantics of the inference rules used in these proofs.
Invariant Projections in Games
Authors: Mohapatra Abhijeet , Decoster Bertrand , Agarwal Sudhir , Genesereth Michael
Published: January 2018

Identification of implicit structures in dynamic systems is a fundamental problem in Artificial Intelligence. In this paper, we focus on General Game Playing where games are modeled as finite state machines. We define a new property of game states called invariant projections which strongly corresponds to humans' intuition of game boards and may be applied in General Game Playing to support powerful heuristics, and to automate the design of game visualizations. We prove that the computation of invariant projections is Pi_{2}^{P}-complete in the size of the game description. We also show that invariant projections form a lattice, and the lattice ordering may be used to reduce the time to compute invariant projections potentially by a factor that is exponential in the schema size of game states. To enable competitive general game players to efficiently identify boards, we propose a sound (but incomplete) heuristic for computing invariant projections and evaluate its performance.
On Implementing Modular Complexity Analysis
Authors: Zankl Harald , Korp Martin
Published: January 2018

We recall the recent approach by (Zankl and Korp, 2010) to prove upper bounds on the (derivational) complexity of term rewrite systems modularly. In this note we show that this approach is suitable to tighten bounds after they have been established. The idea is to replace proof steps with a large bound by (new) proofs that yield smaller bounds. An evaluation of the approach shows the benefits.
Morín, Edgar y Alfredo Nateras (coord.) (2009), Tinta y Carne, México, D. F.: Editorial Contracultura
Authors: Porraz Gómez Iván Francisco
Published: January 2018

.
Nuevos fondos documentales del Archivo Histórico Diocesano para el estudio de la historia de Chiapas en el siglo XX
Authors: López Hernández Iván Christian , López Tovilla Virginia Margarita , Pérez Mendoza Joel , Pérez Moreno Rodolfo
Published: January 2018

.
Experiencia de ser otro: la conversión de las identidades en la Iglesia adventista
Authors: Castañeda Seijas Minerva Yoimy
Published: January 2018

El artículo analiza los relatos de conversión a la Iglesia adventista en Tapilula, Chiapas. Se construye una propuesta teórica  metodológica que, siguiendo a algunos autores, problematiza la experiencia de conversión para comprender el significado que tiene en la vida de los conversos y analizarla a partir de la categorización del proceso de conversión. Se contrastan tres relatos de conversión que resultan representativos del proceso y se interpretan desde la teoría pragmática de W. James.
In between: sobre la inserción y los diseños identitarios de migrantes latinoamericanos en Nueva York
Authors: Narváez Gutiérrez Juan Carlos
Published: January 2018

En el presente artículo se exploran algunos elementos de los que se valen los migrantes latinoamericanos para reconstruir/deconstruir sus identidades en el contexto de una sociedad huésped: urbana y anglosajona. A través del análisis de las dimensiones de inserción e incorporación objetiva y subjetiva, y con base en fragmentos de  entrevistas realizadas en la ciudad de Nueva York, se trata de dejar registro sobre lo concreto y lo interpretativo de la experiencia  narrada por los sujetos de la migración internacional.
Rodrigo Rey Rosa (2009), El material humano, Barcelona: Anagrama.
Authors: Hernández Palacios Ester
Published: January 2018

.
En busca de indicadores públicos de resultados para el control social del poder en los municipios del estado de Campeche
Authors: López Chan Óscar
Published: January 2018

Con base en la aprobación de reformas a los artículos sexto y 134 de la Constitución General de México, se estableció la obligación de todos los órdenes de gobierno de difundir sus indicadores de gestión. En el caso de los gobiernos municipales, estos indicadores no suelen medir resultados concretos para la ciudadanía porque en las leyes no se define con claridad qué son o qué deben medir. En este sentido, se propone un conjunto de indicadores de resultados para los ayuntamientos a partir de sus competencias formales.
Nociones relacionadas con las cuevas en la lengua y cosmovisión tseltales
Authors: Méndez Pérez Marceal
Published: January 2018

En el presente texto se estudian algunas nociones relacionadas con las cuevas entre los tseltales de Chiapas, las cuales sólo en lengua tseltal parecen tener sentido. Dichas nociones permiten conocer y comprender otras funciones importantes de las cuevas, como su carácter de entradas hacia el interior de la tierra y la montaña, o hacia el lugar llamado Inframundo.
Presentación
Authors: Bosch Heras Montserrat
Published: January 2018

.
Un proyecto para abrir un nuevo camino desde la costa caribeña a la ciudad de la Nueva Guatemala en el siglo XVIII
Authors: Reichert Rafal
Published: January 2018

.
Migración y remesas: ¿están afectando la sustentabilidad de la agricultura y la soberanía alimentaria en Chiapas?
Authors: Morales Helda , Aguilar-Stoen Mariel Cristina , Castellanos López Edwin Josué
Published: January 2018

Con este artículo se pretende contribuir al debate sobre el impacto de la migración internacional y de las remesas en la agricultura. Presentamos los resultados de una encuesta realizada en 2011 sobre agricultura, combinados con muestreos de agrobiodiversidad en parcelas de familias con y sin migrantes de cuatro comunidades campesinas de Chiapas. En contra de lo esperado, los resultados sugieren que la migración no está provocando ni abandono de la agricultura, ni cambios sustanciales en el tipo de cultivos de las zonas estudiadas.
Los límites de la alteridad: el otro desde la energética social
Authors: Jullian Montañez Alain G.
Published: January 2018

La alteridad ha sido abordada desde varias perspectivas, como la educación, el lenguaje, la psicopedagogía, la psicología, la sociología, la antropología o la filosofía, por lo que se ha considerado necesario efectuar una recapitulación de los avances en el tema. Al llevar a cabo esa revisión, se hizo evidente que ninguna de las perspectivas aporta una base material al "problema del otro". En este artículo se busca, mediante la perspectiva de la energética social, rastrear dicha base material de la alteridad.
"Desde arriba o desde abajo": construcciones y articulaciones en la investigación sobre educación intercultural en México
Authors: Bermúdez Urbina Flor Marina
Published: January 2018

Se realiza una aproximación a las comunidades epistémicas que conforman el subcampo de la educación intercultural en México y se reflexiona sobre los ámbitos y procesos que la articulan. Se exponen las circunstancias que favorecen una transición de la investigación sobre la educación indígena hacia la educación intercultural y se explican las coyunturas que permiten su emergencia. Posteriormente se describe el campo que articula las comunidades epistémicas diferenciadas por miradas "desde arriba y desde abajo". Se concluye con una reflexión sobre los desafíos que enfrentan el estudio de las comunidades epistémicas y la investigación sobre educación intercultural.
Políticas neoliberales y afectaciones territoriales en México. Algunos "para qués" de "otras" educaciones
Authors: Bertely Busquets María
Published: January 2018

Se analiza la relación entre algunos programas destinados al abatimiento de la pobreza y un proceso de inducción educativa que incrementa y separa a los productores indígenas y campesinos de sus medios de producción. Considerando la trayectoria de una organización étnico-política gestada en Chiapas, México, así como las refundaciones de los nuevos Estados plurinacionales, los diversos escenarios de disputa territorial muestran cómo el reconocimiento de la integridad sociedad-naturaleza interviene en los objetivos de otras formas de educación. En este contexto, la perspectiva sintáctica de la cultura aporta a la defensa de derechos vulnerados por las políticas neoliberales en México.
Movilidad múltiple nacional e internacional de una población mexicano-guatemalteca
Authors: Arriola Vega Luis Alfredo
Published: January 2018

Se examina la movilidad prolongada de una población mexicana de ascendencia guatemalteca. A tal efecto, se obtuvieron datos a través de métodos etnográficos, principalmente vía testimonios de trayectorias de vida. La perspectiva amplia permite encuadrar la movilidad individual en marcos de análisis más extensos, entre ellos el grupo familiar. La movilidad está influenciada por ese contexto familiar y por otros factores, como circunstancias coyunturales específicas o el momento en el ciclo de vida del migrante. Migraciones interrumpidas, circulares y de retorno dificultan la comprensión de esas trayectorias porque generalmente son parte de procesos, como flujos mixtos y migraciones continuadas.