A deterministic Python compiler that converts English sentences into typed algebraic formulas, semantic graphs, and a Z3-backed logical knowledge base.
pip install -r requirements.txt
python -m spacy download en_core_web_lg # recommended
# or: python -m spacy download en_core_web_sm (faster, less accurate)# Single sentence — JSON output + graph PNG
python main.py "The cat drinks milk."
# Interactive mode — coreference tracked across sentences
python main.py
> Who drinks milk?
> Every human dies.
> Mary believes John loves Alice.
> quitInput : The cat drinks milk.
Formula: Drink(Cat, Milk)
Decoded: Cat drinks milk.
Input : Who drinks milk?
Formula: Query(x, Drink(X, Milk))
Decoded: Who drink milk?
Input : Every human dies.
Formula: ForAll(x, Implies(Human(X), Die(X)))
Decoded: Every human dies.
Input : Mary believes John loves Alice.
Formula: Believe(Mary, Love(John, Alice))
Decoded: Mary believes John loves alice.
pytest tests/ -v173 tests, all passing.
| Structure | Example |
|---|---|
| Active SVO | "The cat drinks milk." |
| Passive | "Milk is drunk by the cat." |
| Agentless passive | "The report was published." |
| Copular (class / identity / property) | "John is a doctor." / "Clark Kent is Superman." / "The sky is blue." |
| Existential | "There is a cat on the mat." |
| Wh-question | "Who drinks milk?" / "What does John buy?" |
| Negation | "John does not eat apples." / "Mary never arrived." |
| Coordination | "John eats and drinks." / "John and Mary run." |
| Neither/nor | "Neither Alice nor Bob came." |
| If/then conditional | "If John eats food then John survives." |
| Subjunctive conditional | "Should it rain, we stay indoors." |
| Universal quantifier | "Every human dies." / "Every living thing requires water." |
| Existential quantifier | "Someone loves Mary." |
| Belief / propositional attitude | "Mary believes John loves Alice." |
| Embedded clause | "John said Mary loves Tom." |
| Relative clause | "The man who owns the car drives fast." |
| Adjective modifier | "The red apple fell." |
| Prepositional phrase | "The book is on the table." |
| Time adverb | "John ate an apple yesterday." |
| Compound noun subject | "Clark Kent flies." / "The flight crew landed safely." |
usa_compiler/
├── main.py # CLI entry point (rich output, coref session)
├── requirements.txt
├── tests/
│ └── test_compiler.py # 173 tests
└── usa/
├── compiler/
│ ├── primitives.py # PrimitiveType enum + Primitive dataclass
│ ├── type_system.py # TypeChecker + semantic anomaly detection
│ ├── parser.py # spaCy dependency-tree parser → ParsedSentence
│ ├── encoder.py # ParsedSentence → Formula list
│ ├── operators.py # Formula constructors
│ ├── decoder.py # Formula list → English
│ ├── canonicalizer.py # Surface normalisation (articles, case)
│ ├── semantic_graph.py # Formula list → SemanticGraph
│ ├── formula.py # Formula/Term dataclasses + serialisers
│ ├── coref.py # Coreference resolution (neural + rule-based)
│ ├── z3_translator.py # Formula → Z3 BoolExpr
│ ├── reasoner.py # Z3-backed KB (entails, query, derive)
│ └── tokenizer.py # spaCy tokenizer wrapper
├── models/
│ ├── node.py # SemanticNode
│ ├── edge.py # SemanticEdge
│ └── graph.py # SemanticGraph (NetworkX + PNG visualisation)
├── examples/
│ └── sentences.txt # Example sentences covering all features
└── docs/
└── architecture.md # Full architecture reference
- Tense and aspect representation (spaCy morphology → Time primitives)
- Multilingual support (swap spaCy model; primitives are language-neutral)
- Knowledge graph export (RDF/OWL via rdflib, Neo4j via py2neo)
- LLM-assisted fluent decoding
- Constituency-level phenomena (raising, control, tough-movement)