Paper Info
Title
Computational Solutions for Structural Constraints
Abstract
The need to solve structural constraints arises when we investigate computational solutions to the question: "in which logics is a given formula deducible?" This question is posed when one wants to learn the structural permissions for a Categorial Grammar deduction. This paper is part of a project started at [10], to deal with the question above. Here, we focus on structural constraints, a form of Structurally-Free Theorem Proving, that deal with an unknown transformation X which, when applied to a given set of components P1...Pn, generates a desired structure Q. The constraint is treated in the framework of the combinator calculus as XP1...Pn ↠ Q, where the transformation X is a combinator, the components Pi and Q are terms, and ↠ reads "reduces to". We show that in the usual combinator system not all admissible constraints have a solution; in particular, we show that a structural constraint that represents right-associativity cannot be solved in it nor in any consistent extension of it. To solve this problem, we introduce the notion of a restricted combinator system, which can be consistently extended with complex combinators to represent right-associativity. Finally, we show that solutions for admissible structural constraints always exist and can be efficiently computed in such extension.
Year
DOI
Venue
1998
10.1007/3-540-45738-0_2
LACL
Keywords
Field
DocType
consistent extension,admissible structural constraint,usual combinator system,combinator calculus,components pi,restricted combinator system,structural constraint,components p1,structural constraints,structural permission,computational solutions,admissible constraint,theorem proving,categorial grammar
Structural rule,Combinatory logic,Computer science,Automated theorem proving,Substructural logic,Algorithm,Categorial grammar,Let expression
Conference
ISBN
Citations 
PageRank 
3-540-42251-X
0
0.34
References 
Authors
3
1
Name
Order
Citations
PageRank
Marcelo Finger13010.09