 General
 What is CZFC and Mathdialog?

CZFC is a version of ZFC with an intrinsic handling of context. This makes it easy for both machines and humans, dealing with formal proofs. Mathdialog is a computer implementation of the CZFC set theory.

 What is a proof in CZFC and Mathdialog?

A proof in CZFC is a list of logiccommands. In Mathdialog there are two types of proof the humantomachine proofs and the machinetohuman proofs. The first one help users to find the CZFC proof (see the The Interesting and Fun Game of Mathdialog Proofse), the second one is an interactive hypertext environment that helps other users to understand the proof in a natural mathematical language that is, users doesn't need to know CZFC or Mathdialog to understand it.

 What are logiccommands?

Logiccommands are the building blocks of proofs. In the humantomachine proofs, they generate hypotheses and/or new goals and mirror each proof step used in mathematical books. A logiccommand is a step in a proof that models some step in books such as proof by contradiction, brig a definition, instantiate a quantified formula, etc. For example, if the present goal is
SUBSET(A,B) ==> BG(x,B)
then the logiccommand IF_RED[] place BG(x,B) as a new goal and SUBSET(A,B) as a new hypothesis.

 What are the valid inference rules in Mathdialog?

There are not inference rules in Mathdialog, deductions are done through logiccommands. All logiccommands are described in the
Logiccommands Reference Guide.

 What is a CZFC proof?
 What is a humantomachine proof?

A humantomachine proof is a dialog between humans and machines that helps the former to find a CZFC proof. This dialog take place in the mathdialog.com web GUI that enable users to send sentences to Mathdialog and get a response from it. The proof starts when the user write and send a theorem (one of the kind of sentences Mathdialog understand) in the command window, it responds by displaying the theorem hypotheses and its thesis in the black board, the latter is the proof main goal. Then, the user write and send logiccommands (another kind of sentences Mathdialog understand) one by one until Mathdialog responds with a hypothesis that matches the main goal.

 What is a machinetohuman proof?

A machinetohuman proof is a hypertext interactive environment where almost all necessary facts to understand the proof are at the user finger tips. You do not have to know CZFC nor Mathdialog to understand them.

 Humantomachine proofs
 How to write theorems and definitions in Mathdialog?

To write theorems and some definitions, you have to follow the following syntax depending of the type of object you want to write. In what follow:
LABEL is a string with no blank spaces, the theorem or definition name.
LFA is a List of Atomic Formulas, they are the theorem or definition
hypotheses for humans and the theorem local context for Mathdialog.
FORMULA is a logical formula.
VAR_LIST is the list of variables in its respective LFA.
For example, the informal syntax for theorems is:
THEOR[LABEL;LFA;FORMULA]
Notice that, in Mathdialog, even the most insignificant theorem (there are not corollaries, lemmas, etc) has a name and one or more hypotheses. A formula alone does not make sense in Mathdialog, it must have a context. In theorems and, as we will see next, definitions, LFA has this functionality.
For predicates, the informal syntax is:
DEF_PRED[LABEL;LFA;LABEL(VAR_LIST) <==> FORMULA]
For comprehension sets the informal syntax is:
DEF_OBC[LABEL;LFA;LABEL(VAR_LIST) = {BG(x,TERM):FORMULA}
Suppose TH_EX_UN is the name (label) of a theorem of existence and uniqueness, then informal syntax for a existential object is:
DEF_OBE[LABEL;LFA;LABEL(VAR_LIST) = TH_EX_UN]
In Mathdialog, this definition and the theorem TH_EX_UN must be seen as one object (even though a theorem of existence and uniqueness can exists without a existential object definition), in particular the LFA of the theorem TH_EX_UN and the LFA of this definition must literally match.

 Machinetohuman proofs
 What is the difference between a machinetohuman proof and a proof in a book?

A machinetohuman proof is an interactive environment where you control the steps flow and helps you to solve your doubts about that proof. When you read a proof in a book and you don't understand a step or where a hypothesis come from, you have to wait to ask to your teacher. Instead, in a machinetohuman proof you have all the facts to understand it at your finger tips.

 Accounts and logins
 Why I have to login?

You don't have to. Everybody can consult machinetohuman proofs. However if you want formulate a new definition or a new theorem to start a humantomachine proofs, you have to be logged. One of the incentives to prove theorems in Mathdialog is that your name will be associated to that theorem, the more important the theorem you prove the bigger prestige you will have. At the present stage, all theorems are elementary. Its importance depends of the development one is making on a given time. When a logged user consults a machinetohuman proof the correspondent humantomachine proof is displayed in a floating window, this is useful to learn about how to make humantomachine proofs.

 Web user interface
 How resize a window?

There are two types of windows, one is the background fixed windows, in the humantomachine proofs they are the blackboard and the command window, in the machinetohuman proofs they are the goal, the hypotheses and the step windows. The other type of windows are the floating windows, you can resize them by dragging the lower right corner, you can also move them by dragging its titlebar.

 How can I close the result list window returned from a search?

That cannot be done, you have to choice a list element and delete the resulting window.

 Why sometimes I cannot close a floating window?

A floating window cannot be closed if it has a child. The number in titlebar indicate if it has a parent. For example the numbers 1.2, 1.4.1 and 2.3 mean that they parents are 1, 1.4 and 2 respectively.

 What is the child of a floating window?

A child of a floating window is a floating window that contains a definition or theorem related to its parent. For example if a floating window contains the partial order definition:
Definition of: P_ORDER;
If RELAT_IN(R,A), then we will say that
P_ORDER(R,A)
if and only if
ANTISYMMETRIC(R,A) AND REFLEXIVE(R,A) AND TRANSITIVE(R,A)
and you want to see the definition of REFLEXIVE, just select it, hover consuls in the main menu and click "The selected name". The REFLEXIVE definition will appear in a new floating window that is a child of the one with the P_ORDER definition.

 Why mathdialog.com doesn't respond to my touches?

The Mathdialog GUI does not works with touch screen devices such as tablets or mobile phones. mathdialog.com has been tested with Firefox, Chrome, Opera, Vivaldi, Edge and Safari web browsers.

 What browsers can be used to use mathdialog.com?

Mathdialog.com has been tested with Firefox, Chrome, Opera, Vivaldi, Edge and Safari web browsers.

 Why the red button "Connect here" doesn't work?

The web mathdialog.com is just the user interface, the red button means the browser cannot connect to the Mathdialog program. There are many reasons for this but it must be temporary, at most 5 minutes, if it takes longer a huge problem is happening. It also happen with incompatible browsers.

