User loginNavigation 
Combinator logic inferenceI'm carrying out some experiments in theorem proving using combinator logic with equality, the rationale being that combinator logic is a variablefree substitute for lambda calculus, and getting rid of variables simplifies both semantics and code quite a bit. I've run into a stumbling block for which suggests that I'm missing some inference rules, and would appreciate it if anyone could point me to what I'm missing. Here's what I have so far. In firstorder predicate calculus, practically all inference can be boiled down to two rules: Unification: consistent substitution of terms for variables. Paramodulation: free substitution of equals for equals. Lambda calculus adds a third rule: Evaluation: expanding out a function call. The simplest case on which the resulting system trips up is the set of clauses p(X) and ~p(X), which in firstorder predicate calculus easily resolve to a contradiction. Translating these formulas and each step of the refutation proof into combinator logic gives (using Unlambda's ` notation, `a b means a(b)): p(X) ~p(X) p(X) in the first statement unifies with p(X) in the second statement So far so good? Why does (false=true) trivially simplify to false? So what am I missing? By Russell Wallace at 20090905 18:06  LtU Forum  previous forum topic  next forum topic  other blogs  3343 reads

Browse archivesActive forum topics
New forum topics

Recent comments
23 hours 24 min ago
2 days 18 hours ago
1 week 6 days ago
2 weeks 5 days ago
3 weeks 5 days ago
5 weeks 4 days ago
5 weeks 6 days ago
7 weeks 17 hours ago
7 weeks 4 days ago
7 weeks 4 days ago