Goals and benchmarks for automated map reasoning
From MaRDI portal
Publication:5927984
DOI10.1006/jsco.1999.0362zbMath0965.03014MaRDI QIDQ5927984
Andrea Formisano, Marco Temperini, Eugenio Giovanni Omodeo
Publication date: 19 March 2001
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/1878df0c3a94737a48f246d9532b2cc962c471ee
automated reasoning; equational logic; Tarski-Givant map calculus; translation from first-order logic into map calculus
03B35: Mechanization of proofs and logical operations
03G99: Algebraic logic
08B05: Equational logic, Mal'tsev conditions
Related Items
Unnamed Item, Layered map reasoning, Compiling dyadic first-order specifications into map algebra, ER modelling from first relational principles, Three-variable statements of set-pairing, A graphical representation of relational formulae with complementation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Problem corner: Robbins algebra: Conditions that make a near-Boolean algebra Boolean
- Relation algebras: Concept of points and representability
- Embedding Boolean expressions into logic programming
- Rapid construction of algebraic axioms from samples
- The origin of relation algebras in the development and axiomatization of the calculus of relations
- Baltic computer science. Selected papers
- \(T\)-resolution: Refinements and model elimination
- Computer proofs in Gödel's class theory with equational definitions for composite and cross
- Solution of the Robbins problem
- A logic for rough sets
- The automation of syllogistic. II: Optimization and complexity issues
- Set theory for verification. II: Induction and recursion
- \(T\)-theorem proving. I
- The representation of relational algebras
- On the relative expressiveness of description logics and predicate logics
- Negation as failure: a comparison of Clark's completed data base and Reiter's closed world assumption
- Decision procedures for elementary sublanguages of set theory. I. Multi-level syllogistic and some extensions
- Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions
- Expressing infinity without foundation
- On the Decision Problem for Two-Variable First-Order Logic
- A Finite Axiomatization for Fork Algebras
- Program derivation with verified transformations — a case study
