This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

Student Guide

Getting Started

1. Log in with the username and password provided by your instructor
2. Click Submissions in the navigation bar
3. Click + New to create a new submission

Creating a Submission

Step 1: Problem Description

Fill in the natural-language reasoning:

• Background — the context or scenario of the problem
• Question — what is being asked
• Answer — the natural-language answer

Step 2: Logic Type

Select whether your formalization uses:

• Propositional Logic — for arguments with simple propositions (P, Q, R, ...)
• First-Order Logic — for arguments with predicates, quantifiers, and variables

Step 3: Translation Mapping

Click + Add to define your proposition/predicate letters:

• Left field: the formal symbol (e.g., P)
• Right field: the natural-language meaning (e.g., "It is raining")

Step 4: Reasoning

• Premises — add each premise as a LaTeX formula (click + Add Premise)
• Conclusion — enter the conclusion formula
• Entails — select Yes/No for whether the premises entail the conclusion

Writing Formulas

You can input formulas in multiple formats. The system normalizes them automatically:

Meaning	Accepted Inputs	Normalized Form
And	∧, \wedge, \and, &	\wedge
Or	∨, \vee, |	\vee
Not	¬, \neg, \lnot, ~	\neg
Implies	→, \rightarrow, \to, \implies, ->	\rightarrow
Iff	↔, \leftrightarrow, \iff, <->	\leftrightarrow
For all	∀, \forall	\forall
Exists	∃, \exists	\exists

Examples:

• Propositional: P \rightarrow (Q \wedge R)
• First-order: \forall x(P(x) \rightarrow Q(x))
• Complex subscripts: P_{1,2} \vee Q_1

Click Show LaTeX Preview to see the rendered formula.

Step 5: Validity Check (Optional)

Click Check Validity to run the Z3 SMT solver:

• ✅ Valid — the argument is logically valid
• ❌ Invalid — a counterexample is shown
• ⚠️ Unknown — the solver could not determine validity within resource limits

Step 6: Submit

Click Submit (for new) or Update (for edits) to save your work.

LLM Challenge (Optional)

This is a bonus feature. If you can construct a natural-language reasoning (Background + Question + Answer) that misleads a large language model into giving an incorrect answer:

1. Open a conversation in ChatGPT, Gemini, DeepSeek, Doubao, Qwen, or another LLM
2. Present your reasoning problem and get the LLM to answer incorrectly
3. Use the LLM's "Share" feature to generate a share link
4. Paste the link in the LLM Challenge section
5. The platform auto-detects the LLM platform from the URL

Your teacher will review each link and mark it as Pass or Fail.

Viewing Grades

After your teacher reviews your submission:

• The grade appears in the sidebar (Excellent / Good / Fair / Fail / Pending / Passed)
• Teacher comments appear below the submission
• LLM Challenge verification status appears next to each link

Changing Your Password

Click Password in the navigation bar to change your password. Requirements: at least 8 characters, must contain both letters and numbers.