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  3151 reads

Browse archivesActive forum topics 
Recent comments
2 min 57 sec ago
3 hours 22 min ago
3 hours 39 min ago
8 hours 9 min ago
15 hours 27 min ago
20 hours 58 min ago
21 hours 6 min ago
1 day 1 hour ago
1 day 19 hours ago
1 day 21 hours ago