Idioma:

Multi-Completion with Termination Tools

Winkler, Sarah ; Sato, Haruhiko ; Middeldorp, Aart ; Kurihara, Masahito

Journal of automated reasoning, 2013-03, Vol.50 (3), p.317-354 [Periódico revisado por pares]

Dordrecht: Springer Netherlands

Texto completo disponível

Citações Citado por

Enviar para

Título:
Multi-Completion with Termination Tools
Autor: Winkler, Sarah ; Sato, Haruhiko ; Middeldorp, Aart ; Kurihara, Masahito
Assuntos: Applied sciences ; Artificial Intelligence ; Computer Science ; Computer science; control theory; systems ; Exact sciences and technology ; Language theory and syntactical analysis ; Mathematical Logic and Formal Languages ; Mathematical Logic and Foundations ; Symbolic and Algebraic Manipulation ; Theoretical computing
É parte de: Journal of automated reasoning, 2013-03, Vol.50 (3), p.317-354
Descrição: Knuth–Bendix completion is a classical calculus in automated deduction for transforming a set of equations into a confluent and terminating set of directed equations which can be used to decide the induced equational theory. Multi-completion with termination tools constitutes an approach that differs from the classical method in two respects: (1) external termination tools replace the reduction order—a typically critical parameter—as proposed by Wehrman et al. ( 2006 ), and (2) multi-completion as introduced by Kurihara and Kondo ( 1999 ) is used to keep track of multiple orientations in parallel while exploiting sharing to boost efficiency. In this paper we describe the inference system, give the full proof of its correctness and comment on completeness issues. Critical pair criteria and isomorphisms are presented as refinements together with all proofs. We furthermore describe the implementation of our approach in the tool , present extensive experimental results and report on new completions.
Editor: Dordrecht: Springer Netherlands
Idioma: Inglês

Links

View record in Pascal Francis

Voltar para lista de resultados

Anterior Resultado 3 Avançar Ir para próxima página

Realização: Logos de Redes Sociais:

Multi-Completion with Termination Tools

Winkler, Sarah ; Sato, Haruhiko ; Middeldorp, Aart ; Kurihara, Masahito

Dordrecht: Springer Netherlands

Buscando em bases de dados remotas. Favor aguardar.