The satisfiability version of the tableau method for zeroeth order logic can be viewed as a non-deterministic algorithm.
The initial state is one with the statement to the left of the line.
At each step the actions are to take an unused statement, mark it used, and write down its consequences, in the non-branching case, or one of the two possibilities, in the branching case.
The termination condition is running out of unused statements (successful) or finding a contradiction (unsuccessful).
If the algorithm can terminate successfully then the statement is satisfiable.
In this case, unlike many non-deterministic computations, the algorithm will always terminate, successfully or not.
Similar remarks apply to proving tautologies, but we start with the statement to the right of the line and “success” and “failure” mean the opposite of what you’d expect.
The Łukasiewicz formal system or, more generally, any axiomatic system can also be considered a non-deterministic algorithm.
The initial state is an empty list of statements.
In each state our options are to write down an axiom or apply a rule of inference to one or two previous statements.
Successful termination is writing down the statement we were trying to prove.
Unsuccessful termination is impossible, but non-termination is very common.
The given statement is a theorem if the algorithm can terminate successfully.
One complication is that substitution allows replacement of a variable by any expression and there are infinitely many expressions, so again we have to consider trees where some nodes may have infinitely many children.