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

Browse archivesActive forum topics 
Recent comments
1 hour 39 min ago
2 hours 25 min ago
2 hours 25 min ago
8 hours 38 min ago
9 hours 1 min ago
9 hours 20 min ago
11 hours 48 min ago
22 hours 10 min ago
1 day 7 min ago
1 day 7 hours ago