tpg
tpg copied to clipboard
wo
Tree Proof Generator
`∀xc(x,1)=1,∀x(x=1↔¬x=0),∀xc(0,x)=1|= c(a,c(b,b))=1` is valid, but the modelfinder presents a countermodel.
Hi, I'm interested in using your tool for first order logic validation. Thank you for sharing. Could you please share any more information on the set of symbols and how...
As I can see, there is no way to enter logical constants (I've tried `top`/`bottom`/`0`/`1`). Of couse, one can use `p -> p` for top, but it isn't convenient. Although...
Was using Exy as a shorthand for set membership x e y. Was looking at this proof: ∃x(Exy → ∀zEzy) is valid. https://www.umsu.de/trees/#~7x%28Exy~5~6zEzy%29 In step 3 it shows Eyy. Could...
I wanted to experiment with a certain Kripke semantics for intuitionistic logic. But I am missing a check box to choose a persistency condtion for the accessibility relation. This would...
Hi. I love this proof generator, and feel almost ashamed to ask for a feature. Also, not sure what barriers there might be to it in terms of coding. But...
I tried this here: > ∀x(m(e,x)=x)∧∀x(m(i(x),x)=e)∧∀x∀y∀z(m(m(x,y),z)=m(x,m(y,z)))→∀x(m(x,e)=x) https://www.umsu.de/trees/#~6x(m(e,x)=x)~1~6x(m(i(x),x)=e)~1~6x~6y~6z(m(m(x,y),z)=m(x,m(y,z)))~5~6x(m(x,e)=x) But it gets very quickly into a state where stop buttion doesn't work anymore. Bug or feature?
Hi, I am quite amazed by your tool, since it not only searches a proof, it also tries to find a counter model at the same time. I am currently...
What is the search strategy for proofs? Some iterative deepening. Here is a funny example, where I find a shorter regular proof for FOL with equality, its a validation proof,...
Hello, after "php -S localhost:1234 router.php" I get the following error message from the browser: JS loading error: file /Users/andrea/Downloads/tpg-master/array-formula-parser-prover-modelfinder-sentree-painter-index.js not found js is activated, mamp is configured and running,...
