- Query

In order to submit a query one should first describe the symbols used in the query by providing a specification. Once a specification is defined it can be used for computing any number of queries.
- Example of query
Hvide |- (A |=> (B |=> C)) |=> (A |=> B) |=> A |=> C end
(A or B) && C && (D && P) |- (A or B) or ^(Q) or (A && B) end
(A |=> (B |=> C)) && (A && B) && ^(C) |- FALSE end
(A |=> (B |=> C)) && ^((A && B) |=> C) |- FALSE end
A && B |- A or B end
(P |=> Q) |- ^(Q) |=> ^(P) end
P |=> Q |- ^(Q) |=> ^(P) end
(^(B) |=> ^(A)) |- (C |=> A) |=> (C |=> B) end