The Core Method: Connectionist Model Generation for First-Order Logic Programs

2019 ◽

Author(s):

Sebastijan Dumancic ◽

Tias Guns ◽

Wannes Meert ◽

Hendrik Blockeel

Keyword(s):

Deep Learning ◽

Relational Learning ◽

Order Logic ◽

First Order Logic ◽

Relational Data ◽

Logic Programs ◽

Learning Methods ◽

First Order ◽

Relational Structures ◽

Representation Language

Deep learning methods capable of handling relational data have proliferated over the past years. In contrast to traditional relational learning methods that leverage first-order logic for representing such data, these methods aim at re-representing symbolic relational data in Euclidean space. They offer better scalability, but can only approximate rich relational structures and are less flexible in terms of reasoning. This paper introduces a novel framework for relational representation learning that combines the best of both worlds. This framework, inspired by the auto-encoding principle, uses first-order logic as a data representation language, and the mapping between the the original and latent representation is done by means of logic programs instead of neural networks. We show how learning can be cast as a constraint optimisation problem for which existing solvers can be used. The use of logic as a representation language makes the proposed framework more accurate (as the representation is exact, rather than approximate), more flexible, and more interpretable than deep learning methods. We experimentally show that these latent representations are indeed beneficial in relational learning tasks.

Download Full-text

The Core Method: Connectionist Model Generation

Artificial Neural Networks – ICANN 2006 - Lecture Notes in Computer Science ◽

10.1007/11840930_1 ◽

2006 ◽

pp. 1-13 ◽

Cited By ~ 3

Author(s):

Sebastian Bader ◽

Steffen Hölldobler

Keyword(s):

Model Generation ◽

Connectionist Model ◽

The Core ◽

Core Method

Download Full-text

SGGS Theorem Proving: an Exposition

10.29007/m2vf ◽

2018 ◽

Author(s):

Maria Paola Bonacina ◽

David Plaisted

Keyword(s):

Theorem Proving ◽

Order Logic ◽

First Order Logic ◽

Candidate Model ◽

Narrative Style ◽

First Order ◽

The Core ◽

Theorem Provers ◽

Instance Generation ◽

Main Ideas

We present in expository style the main ideas in SGGS, which stands for Semantically-Guided Goal-Sensitive theorem proving. SGGS uses sequences of constrained clauses to represent models, instance generation to go from a candidate model to the next, and resolution as well as other inferences to repair the model. SGGS is refutationally complete for first-order logic, DPLL-style model based, semantically guided, goal sensitive, and proof confluent, which appears to be a rare combination of features. In this paper we describe the core of SGGS in a narrative style, emphasizing ideas and trying to keep technicalities to a minimum, in order to advertise it to builders and users of theorem provers.

Download Full-text

Strong Equivalence and Program’s Structure in Arguing Essential Equivalence Between First-Order Logic Programs

Practical Aspects of Declarative Languages - Lecture Notes in Computer Science ◽

10.1007/978-3-030-05998-9_1 ◽

2018 ◽

pp. 1-18

Author(s):

Yuliya Lierler

Keyword(s):

Order Logic ◽

First Order Logic ◽

Logic Programs ◽

First Order

Download Full-text

A Novel Categorical Approach to Semantics of Relational First-Order Logic

Symmetry ◽

10.3390/sym12101584 ◽

2020 ◽

Vol 12 (10) ◽

pp. 1584

Author(s):

Wolfgang Schreiner ◽

William Steingartner ◽

Valerie Novitzká

Keyword(s):

Term Structure ◽

Set Theory ◽

Order Logic ◽

First Order Logic ◽

Basic Logic ◽

Categorical Approach ◽

First Order ◽

The Core ◽

Deduction Rules ◽

Categorical Semantics

We present a categorical formalization of a variant of first-order logic. Unlike other texts on this topic, the goal of this paper is to give a very transparent and self-contained account without requiring more background than basic logic and set theory. Our focus is to show how the semantics of first-order formulas can be derived from their usual deduction rules. For understanding the core ideas, it is not necessary to investigate the internal term structure of atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations; in this sense, our variant of first-order logic is “relational”. While the derived semantics is based on categorical principles (even the duality that arises from a symmetry between two ways of looking at something where there is no reason to choose one over the other), it is nevertheless “constructive” in that it describes explicit computations of the truth values of formulas. We demonstrate this by modeling the categorical semantics in the RISCAL (RISC Algorithm Language) system which allows us to validate the core propositions by automatically checking them in finite models.

Download Full-text

Verification of Imperative Programs through Transformation of Constraint Logic Programs

10.29007/163x ◽

2018 ◽

Author(s):

Emanuele De Angelis ◽

Fabio Fioravanti ◽

Alberto Pettorossi ◽

Maurizio Proietti

Keyword(s):

Program Transformation ◽

Program Verification ◽

Order Logic ◽

Initial Configuration ◽

First Order Logic ◽

Logic Programs ◽

Partial Correctness ◽

First Order ◽

Transformation Rules ◽

Constraint Logic Programs

We present a method for verifying partial correctness properties of imperative programs by using techniques based on the transformation of constraint logic programs (CLP). We consider: (i) imperative programs that manipulate integers and arrays, and (ii) first order logic properties that define <i>configurations</i> of program executions. We use CLP as a metalanguage for representing imperative programs, their executions, and their properties. First, we encode the correctness of an imperative program, say Prog, as the negation of a predicate 'incorrect' defined by a CLP program T. By construction, 'incorrect' holds in the least model of T if and only if the execution of Prog from an initial configuration eventually halts in an error configuration. Then, we apply to program T a sequence of transformations that preserve its least model semantics. These transformations are based on well-known transformation rules, such as unfolding and folding, guided by suitable transformation strategies, such as specialization and generalization. The objective of the transformations is to derive a new CLP program TransfT where the predicate 'incorrect' is defined either by (i) the fact `incorrect.' (and in this case Prog is incorrect), or by (ii) the empty set of clauses (and in this case Prog is correct). In the case where we derive a CLP program such that neither (i) nor (ii) holds, we iterate the transformation. Since the problem is undecidable, this process may not terminate. We show through examples that our method can be applied in a rather systematic way, and is amenable to automation by transferring to the field of program verification many techniques developed in the field of program transformation.

Download Full-text