Matematické Fórum

Zdravím,
chtěl bych se zeptat zda správně rozumím některým záležitostem v PL.
1) Pokud mám formuli a chci ukázat, že je kontradikce, tak existuje nějaký algoritmický postup jak to dokázat nebo to pouze "odhaduji"? Pokud chci ukázat, že formule je logicky platná použiji sémantický strom lze to využít právě i u kontradikce?
2) Pokud chci vytvořit sémantický strom formule [mathjax](\forall x)(v(x)\Rightarrow (\exists y)o(y,A)) \wedge v(A)\wedge ...[/mathjax].
Mohu postupovat takto:
[mathjax]v(A)[/mathjax]
        |
[mathjax](\forall x)(v(x)\Rightarrow (\exists y)o(y,A)) [/mathjax]
        |
[mathjax](v(A)\Rightarrow (\exists y)o(y,A)) [/mathjax]

Tedy x nahradím A?

3)Ještě bych se chtěl zeptat jak postupuji při rozhdodování o splnitelnosti/kontradikci/platnosti u těchto formulí?

[mathjax]A(x)\Rightarrow (\forall x) A(x)
[/mathjax]