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} |
| 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]; ... |
| Hello Jonathan, Thank you for your comprehensive answer. Particular your hardcopy of the FindEquationalProof-12.1-example adapted to my axiom-problem makes me very hopeful, that this problem can be solved with your new predicates IsBoolean[x]... |
| Thank you, Neil. My first trials with your recommended moveconst-function worked very well. Regards Uwe |