scholarly journals Logical Approach to Theorem Proving with Term Rewriting on KR-logic

2019 ◽  
Author(s):  
Tadayuki Yoshida ◽  
Ekawit Nantajeewarawat ◽  
Masaharu Munetomo ◽  
Kiyoshi Akama
Keyword(s):  
Theorem Proving ◽  
Term Rewriting ◽  
Logical Approach

scholarly journals Subtree matching by pushdown automata

2010 ◽  
Vol 7 (2) ◽  
pp. 331-357 ◽  
Author(s):  
Tomás Flouri ◽  
Jan Janousek ◽  
Bořivoj Melichar
Keyword(s):  
Programming Languages ◽  
Theorem Proving ◽  
Systematic Approach ◽  
Finite Automata ◽  
Term Rewriting ◽  
Mechanical Theorem Proving ◽  
Pushdown Automaton ◽  
String Pattern ◽  
Pushdown Automata ◽  
Mechanical Theorem

Subtree matching is an important problem in Computer Science on which a number of tasks, such as mechanical theorem proving, term-rewriting, symbolic computation and nonprocedural programming languages are based on. A systematic approach to the construction of subtree pattern matchers by deterministic pushdown automata, which read subject trees in prefix and postfix notation, is presented. The method is analogous to the construction of string pattern matchers: for a given pattern, a nondeterministic pushdown automaton is created and is then determinised. In addition, it is shown that the size of the resulting deterministic pushdown automata directly corresponds to the size of the existing string pattern matchers based on finite automata.

Complete Pattern Matching for DNA Computing

2006 ◽  
Vol 05 (04) ◽  
pp. 337-343
Author(s):  
Nadia Nedjah ◽  
Luiza De Macedo Mourelle
Keyword(s):  
Information Retrieval ◽  
Logic Programming ◽  
Pattern Matching ◽  
Theorem Proving ◽  
Dna Computing ◽  
Term Rewriting ◽  
Matching Method ◽  
Subject Term ◽  
Matching Technique ◽  
Complete Matching

Pattern matching is essential in many applications such as information retrieval, logic programming, theorem-proving, term rewriting and DNA-computing. It usually breaks down into two categories: root and complete pattern matching. Root matching determines whether a subject term is an instance of a pattern in a pattern set while complete matching determines whether a subject term contains a sub-term that is an instance of a pattern in a pattern set. For the sake of efficiency, root pattern matching need to be deterministic and lazy. Furthermore, complete pattern matching also needs to be parallel. Unlike root pattern matching, complete matching received little interest from the researchers of the field. In this paper, we present a novel deterministic multi-threaded complete matching method. This method subsumes a deterministic lazy root matching technique that was developped by the authors in an earlier work. We evaluate the performance of proposed method using theorem-proving and DNA-computing applications.

scholarly journals PLATO: A tool to assist programming as term rewriting and theorem proving

1995 ◽  
pp. 797-798 ◽  
Author(s):  
Andre J. Sampaio ◽  
Armando M. Haeberer ◽  
Claudio T. Prates ◽  
Cristina D. Ururahy ◽  
Marcelo F. Frias ◽  
...  
Keyword(s):  
Theorem Proving ◽  
Term Rewriting

Parallelizing functional programs by generalization

1999 ◽  
Vol 9 (6) ◽  
pp. 649-673 ◽  
Author(s):  
ALFONS GESER ◽  
SERGEI GORLATCH
Keyword(s):  
Theorem Proving ◽  
Term Rewriting ◽  
Divide And Conquer ◽  
Constructive Theory ◽  
Generalization Problem ◽  
Parallel Prefix

List homomorphisms are functions that are parallelizable using the divide-and-conquer paradigm. We study the problem of finding homomorphic representations of functions in the Bird–Meertens constructive theory of lists, by means of term rewriting and theorem proving techniques. A previous work proved that to each pair of leftward and rightward sequential representations of a function, based on cons- and snoc-lists, respectively, there is also a representation as a homomorphism. Our contribution is a mechanizable method to extract the homomorphism representation from a pair of sequential representations. The method is decomposed to a generalization problem and an inductive claim, both solvable by term rewriting techniques. To solve the former we present a sound generalization procedure which yields the required representation, and terminates under reasonable assumptions. The inductive claim is provable automatically. We illustrate the method and the procedure by the systematic parallelization of the scan-function (parallel prefix) and of the maximum segment sum problem.

scholarly journals Rewriting and Well-Definedness within a Proof System

10.29007/b7wc ◽  
2018 ◽  
Author(s):  
Issam Maamria ◽  
Michael Butler
Keyword(s):  
Theorem Proving ◽  
Automated Theorem Proving ◽  
Term Rewriting ◽  
Proof System ◽  
Proof Technique ◽  
Partial Functions ◽  
Deductive Proof ◽  
Theorem Provers ◽  
Theoretical Foundations

Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving between deduction and computation (i.e., rewriting) steps. If the logic of reasoning supports partial functions, it is necessary that rewriting copes with potentially ill-defined terms. In this paper, we provide a basis for integrating rewriting with a deductive proof system that deals with well-definedness. The definitions and theorems presented in this paper are the theoretical foundations for an extensible rewriting-based prover that has been implemented for the set theoretical formalism Event-B.

Sign in / Sign up

Export Citation Format

Share Document