CLI Usage¶

Overview¶

pyNMMS provides the pynmms command with three subcommands:

pynmms tell   # Add atoms or consequences to a base
pynmms ask    # Query derivability
pynmms repl   # Interactive REPL

Notation¶

Notational conventions.

A, B, ... range over sentences of the object language.
p, q, r, ... range over atomic sentences.
Γ, Δ range over finite sets of sentences.

The two turnstiles:

Γ |~ Δ — a base consequence. The tell command adds the pair (Γ, Δ) to the base consequence relation |~_B. In the theory, |~_B is a given relation (Definition 1, Ch. 3); in the tool it is built incrementally.
Γ => Δ — a sequent. The ask command tests whether the sequent Γ ⇒ Δ is derivable, i.e., whether there exists a proof tree whose leaves are all axioms of the base.

Note: |~ is input (asserting into the base); => is query (testing derivability from the base). Both Γ and Δ may be empty.

Propositional Object Language¶

The propositional object language is defined by the following unambiguous grammar:

sentence   ::=  impl
impl       ::=  disj ( '->' disj )*            (* right-associative *)
disj       ::=  conj ( '|' conj )*             (* left-associative *)
conj       ::=  unary ( '&' unary )*           (* left-associative *)
unary      ::=  '~' unary | atom | '(' sentence ')'
atom       ::=  IDENTIFIER

Where IDENTIFIER is any non-empty string of letters, digits, and underscores beginning with a letter or underscore. Precedence (tightest to loosest): ~, &, |, ->.

Connective glossary:

Symbol	Name	Arity
`~`	negation	prefix unary
`&`	conjunction	binary, left-associative
\|	disjunction	binary, left-associative
`->`	conditional (implication)	binary, right-associative

The NMMS_Onto Object Language¶

The --onto flag enables NMMS_Onto, an ontology engineering extension of the propositional NMMS object language with concept and role assertions. The vocabulary is borrowed from W3C RDFS and OWL for familiarity; the semantics are those of NMMS (exact-match defeasibility, no weakening, no transitivity).

Atoms. In propositional NMMS, atoms are bare identifiers. In NMMS_Onto, atoms are ground atomic formulas:

Form	Name	Example
C(a)	concept assertion	`Happy(alice)`
R(a, b)	role assertion	`hasChild(alice,bob)`

Bare propositional letters are not valid in NMMS_Onto.

Grammar. The NMMS_Onto grammar replaces the propositional atom production:

atom       ::=  CONCEPT '(' INDIVIDUAL ')'                  (* concept assertion *)
             |  ROLE '(' INDIVIDUAL ',' INDIVIDUAL ')'      (* role assertion *)
sentence   ::=  ...                                          (* all propositional forms *)

Ontology Schemas. In ontology mode, the tell command also supports schema registration. Schemas are macros that generate families of ordinary base axioms:

Schema	CLI syntax	Generated axiom pattern
`subClassOf`	`schema subClassOf C D`	{C(x)} \|~ {D(x)} for any x
`range`	`schema range R C`	{R(x,y)} \|~ {C(y)} for any x,y
`domain`	`schema domain R C`	{R(x,y)} \|~ {C(x)} for any x,y
`subPropertyOf`	`schema subPropertyOf R S`	{R(x,y)} \|~ {S(x,y)} for any x,y
`disjointWith`	`schema disjointWith C D`	{C(x), D(x)} \|~ {} for any x
`disjointProperties`	`schema disjointProperties R S`	{R(x,y), S(x,y)} \|~ {} for any x,y

`pynmms tell`¶

Add atoms or consequences to a JSON base file.

# Create a new base and add a consequence
pynmms tell -b base.json --create "A |~ B"

# Add more consequences (base file must exist)
pynmms tell -b base.json "B |~ C"

# Add atoms
pynmms tell -b base.json "atom X"

# Add atoms with annotations
pynmms tell -b base.json 'atom p "Tara is human"'

# Empty consequent (incompatibility)
pynmms tell -b base.json "s, t |~"

# Empty antecedent (unconditional assertion)
pynmms tell -b base.json "|~ p"

Syntax¶

Consequence: A |~ B or A, B |~ C, D (comma-separated)
Incompatibility: A, B |~ (empty consequent)
Unconditional assertion: |~ A (empty antecedent)
Atom: atom X
Atom with annotation: atom X "description"

Options¶

Flag	Description
`-b`, `--base`	Path to JSON base file (required)
`--create`	Create the base file if missing
`--onto`	Use ontology mode (concept/role assertions with schema-level macros)
`--json`	Output as JSON (pipe-friendly)
`-q`, `--quiet`	Suppress output; rely on exit code
`--batch FILE`	Read statements from FILE (use `-` for stdin)

`pynmms ask`¶

Query whether a sequent is derivable.

pynmms ask -b base.json "A => B"
# Output: DERIVABLE

pynmms ask -b base.json "A => C"
# Output: NOT DERIVABLE

Exit codes¶

Following the grep/diff/cmp convention:

Exit code	Meaning
0	Derivable
1	Error
2	Not derivable

Options¶

Flag	Description
`-b`, `--base`	Path to JSON base file (required)
`--trace`	Print the proof trace
`--max-depth N`	Set the maximum proof depth (default: 25)
`--onto`	Use ontology mode (concept/role assertions with schema-level macros)
`--json`	Output as JSON (pipe-friendly)
`-q`, `--quiet`	Suppress output; rely on exit code
`--batch FILE`	Read sequents from FILE (use `-` for stdin)

JSON output¶

pynmms ask -b base.json --json "A => B"
# Output: {"status":"DERIVABLE","sequent":{"antecedent":["A"],"consequent":["B"]},"depth_reached":0,"cache_hits":0}

With --trace, adds a "trace" array.

Stdin input¶

echo "A => B" | pynmms ask -b base.json -

Batch mode¶

pynmms ask -b base.json --batch queries.txt
pynmms ask -b base.json --json --batch queries.txt
cat queries.txt | pynmms ask -b base.json --batch -

pynmms ask -b base.json --trace "=> A -> B"
# Output:
# DERIVABLE
#
# Proof trace:
#   [R→] on A -> B
#     AXIOM: A => B
#
# Depth reached: 1
# Cache hits: 0

`pynmms repl`¶

Interactive REPL for exploring reason relations.

pynmms repl
pynmms repl -b base.json  # Load existing base

REPL Commands¶

Command	Description
tell A \|~ B	Add a consequence
tell A, B \|~	Add incompatibility (empty consequent)
tell \|~ A	Add unconditional assertion (empty antecedent)
tell atom A	Add an atom
tell atom A "desc"	Add an atom with annotation
ask A => B	Query derivability
show	Display the current base (with annotations)
trace on/off	Toggle proof trace display
save <file>	Save base to JSON
load <file>	Load base from JSON
help	Show available commands
quit	Exit the REPL

Example Session¶

$ pynmms repl
Starting with empty base.
pyNMMS REPL. Type 'help' for commands.

pynmms> tell atom p "Tara is human"
Added atom: p -- Tara is human
pynmms> tell atom q "Tara's body temp is 37C"
Added atom: q -- Tara's body temp is 37C
pynmms> tell p |~ q
Added: {'p'} |~ {'q'}
pynmms> tell s, t |~
Added: set() |~ set()
pynmms> ask p => q
DERIVABLE
pynmms> ask p, r => q
NOT DERIVABLE
pynmms> show
Language (4 atoms):
  p -- Tara is human
  q -- Tara's body temp is 37C
  s
  t
Consequences (2):
  {'p'} |~ {'q'}
  {'s', 't'} |~ set()
pynmms> save mybase.json
Saved to mybase.json
pynmms> quit

Batch files¶

Tell batch format¶

One statement per line. Blank lines and # comments are skipped:

# mybase.base
atom p "Tara is human"
atom q "Tara's body temp is 37C"
p |~ q
s, t |~

pynmms tell -b base.json --create --batch mybase.base

Ontology batch format¶

With --onto, batch files also support schema lines (with optional quoted annotations):

atom Man(socrates) "Socrates is a man"
atom hasChild(alice,bob)
Man(socrates) |~ Mortal(socrates)
schema subClassOf Man Mortal "All men are mortal"
schema range hasChild Person "Children are persons"
schema domain hasChild Parent "Parents have children"
schema subPropertyOf hasChild hasDescendant "Children are descendants"
schema disjointWith Alive Dead "Life and death are incompatible"
schema disjointProperties employs isEmployedBy "Cannot both employ and be employed by"

pynmms tell -b onto_base.json --create --onto --batch onto_base.base

Ask batch format¶

One sequent per line:

# queries.txt
A => B
A, B => C
=> A -> B

pynmms ask -b base.json --batch queries.txt
pynmms ask -b base.json --json --batch queries.txt  # JSONL output

CLI Usage¶

Overview¶

Notation¶

Propositional Object Language¶

The NMMS_Onto Object Language¶

pynmms tell¶

Syntax¶

Options¶

pynmms ask¶

Exit codes¶

Options¶

JSON output¶

Stdin input¶

Batch mode¶

pynmms repl¶

REPL Commands¶

Example Session¶

Batch files¶

Tell batch format¶

Ontology batch format¶

Ask batch format¶

`pynmms tell`¶

`pynmms ask`¶

`pynmms repl`¶