User Portlet
| Discussions |
|---|
| I tried my first simple proof in first-order/predicate logic with FindEquationalProof (12.3) and the following example: Axiom: Everyone has a father Axiom: A grandfather is the father of a father Hypothesis: Everyone has a grandfather ... |
| Thank You, that is working fine: In[913]:= Replace[And[a, b], {HoldPattern[And[x__]] :> List[x]}] Out[913]= {a, b} |
| Hi Jonathan, I have been learning Proof Theory on my own and am working on a document that mathematically explores some notions of proof theory. I have also described in detail the slowest way to prove something: brute force. Then I recently... |
| Thank you Ian for your workarround and particular for your distingtion according the understanding of "free". The behavior of your workarround seems to be very similar to "HoldForm[]": In[163]:= SetAttributes[Formula, HoldAll]; ... |
| Thank you, Neil. My first trials with your recommended moveconst-function worked very well. Regards Uwe |