How to decide the lark

DOI10.1016/0304-3975(93)90015-LzbMath0821.03009MaRDI QIDQ1208736

M. Wymann-Böni, Martin Sprenger

Publication date: 16 May 1993

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

canonical rewrite systemcompletion of an equational theorydecision algorithm for Smullyan's lark combinatorfragments of combinatory logicpolynomial decision procedure

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Word problems, etc. in computability and recursion theory (03D40) Combinatory logic and lambda calculus (03B40)

Related Items (5)

The combinator M and the Mockingbird lattice ⋮ Mockingbird lattices ⋮ Using groups for investigating rewrite systems ⋮ Displaying and deciding substructural logics. I: Logics with contraposition ⋮ The combinator S

Cites Work

• History and basic features of the critical-pair/completion procedure
• The word problem for Smullyan's lark combinator is decidable
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• On theories with a combinatorial definition of 'equivalence'
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: How to decide the lark