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

Browse archives
Active forum topics

Recent comments
13 weeks 4 days ago
17 weeks 6 days ago
19 weeks 3 days ago
19 weeks 3 days ago
22 weeks 1 day ago
26 weeks 5 days ago
26 weeks 5 days ago
27 weeks 1 day ago
27 weeks 1 day ago
30 weeks 3 hours ago