First merge from sts_merge: uploaded files

Author: Pascual Martinez-Gomez

README.md

@@ -11,6 +11,7 @@ and install the packages in the virtual environment with `pip`:
 
 ```bash
 git clone https://github.com/mynlp/ccg2lambda.git
+cd ccg2lambda
 virtualenv --no-site-packages --distribute -p /usr/bin/python3 py3
 source py3/bin/activate
 pip install lxml simplejson pyyaml -I nltk==3.0.5
@@ -25,7 +26,6 @@ python -c "import nltk; nltk.download('wordnet')"
 To ensure that all software is working as expected, you can run the tests:
 
 ```bash
-cd ccg2lambda/
 python scripts/run_tests.py
 ```
 (all tests should pass, except a few expected failures).
@@ -46,10 +46,10 @@ Our system assigns semantics to CCG structures. At the moment, we support C&C fo
 
 ### Installing [C&C parser](http://www.cl.cam.ac.uk/~sc609/candc-1.00.html) (for English)
 
-In order to install the C&C parser, you may need to register, download the parser and the models, and follow their instructions to set it up. For ccg2lambda to find the C&C parser, please create a file `candc_location.txt` with the path to the C&C parser:
+In order to install the C&C parser, you may need to register, download the parser and the models, and follow their instructions to set it up. For ccg2lambda to find the C&C parser, please create a file `en/candc_location.txt` with the path to the C&C parser:
 
 ```bash
-echo "/path/to/candc-1.00/" > candc_location.txt
+echo "/path/to/candc-1.00/" > en/candc_location.txt
 ```
 
 ### Installing [Jigg parser](https://github.com/mynlp/jigg) (for Japanese)
@@ -60,7 +60,7 @@ Simply do:
 ./ja/download_dependencies.sh
 ```
 
-The command above will download Jigg, its models, and create the file `jigg_location.txt` where the path to Jigg is specified. That is all.
+The command above will download Jigg, its models, and create the file `ja/jigg_location.txt` where the path to Jigg is specified. That is all.
 
 ## Using the Semantic Parser
 
@@ -86,16 +86,16 @@ First we need to obtain the CCG derivations (parse trees) of the sentences
 in the text file using C&C and convert its XML format into Jigg's XML format:
 
 ```bash
-cat sentences.txt | perl tokenizer.perl -l en 2>/dev/null > sentences.tok
+cat sentences.txt | sed -f en/tokenizer.sed > sentences.tok
 /path/to/candc-1.00/bin/candc --models /path/to/candc-1.00/models --candc-printer xml --input sentences.tok > sentences.candc.xml
-python candc2transccg.py sentences.candc.xml > sentences.xml
+python en/candc2transccg.py sentences.candc.xml > sentences.xml
 ```
 
 Then, we are ready to obtain the semantic representations by using semantic
 templates and the CCG derivations obtained above:
 
 ```bash
-python semparse.py sentences.xml semantic_templates_en_emnlp2015.yaml sentences.sem.xml
+python scripts/semparse.py sentences.xml en/semantic_templates_en_emnlp2015.yaml sentences.sem.xml
 ```
 
 The semantic representations are in the `sentences.sem.xml` file,
@@ -136,7 +136,7 @@ pipe it to a theorem prover (Coq) and judge the entailment
 relation, you can run the following command:
 
 ```bash
-python prove.py sentences.sem.xml --graph_out graphdebug.html
+python scripts/prove.py sentences.sem.xml --graph_out graphdebug.html
 ```
 
 That command will output `yes` (entailment relation - the conclusion
@@ -163,7 +163,7 @@ For example, to visualize the CCG trees only (without
 semantic representations):
 
 ```bash
-python visualize.py sentences.xml > sentences.html
+python scripts/visualize.py sentences.xml > sentences.html
 ```
 
 and then open the file `sentences.html` with your favourite web browser.
@@ -173,15 +173,16 @@ You should be able to see something like this:
 
 ## Reproducibility
 
-If you wish to reproduce our results reported in EMNLP 2015 or EMNLP 2016, please follow the instructions below:
+If you wish to reproduce our reported results, please follow the instructions below:
 
 * [Experiments on FraCaS at EMNLP 2015](en/fracas.md)
 * [Experiments on JSeM at EMNLP 2016](ja/jsem.md)
+* [Experiments on SICK at EACL 2017](en/sick.md)
 * [Experiments on SICK STS at EMNLP 2017](en/sick_sts.md)
 
 ## Interpreting (and writing your own) semantic templates.
 
-You can find our semantic templates in `semantic_templates_en.yaml`. Here are some notes:
+You can find one of our semantic templates in `en/semantic_templates_en.yaml`. Here are some notes:
 
 1. Each Yaml block is a rule. If the rule matches the attributes of a CCG node, then the semantic template specified by "semantics" is applied. It is possible to write an arbitrary set of field names and their values. For example, you could specify the "category" of the CCG node and the surface "surf" form of a word (in case the CCG node is a leaf). Only the "category" field and the "semantics" field are compulsory.
 2. If you underspecify the characteristics of a CCG node, the semantic rule will match more general CCG nodes. It is also possible to underspecify the features of syntactic categories.
@@ -217,6 +218,24 @@ If you use this software or the semantic templates for your work, please conside
 }
 ```
 
+## A mechanism to inject axioms on-demand:
+
+* Pascual Martínez-Gómez, Koji Mineshima, Yusuke Miyao, Daisuke Bekki. On-demand Injection of Lexical Knowledge for Recognising Textual Entailment. Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics, pages 710-720, Valencia, Spain, 3-7 April, 2017. [pdf](http://www.aclweb.org/anthology/E17-1067)
+
+```
+@InProceedings{martinezgomez-EtAl:2017:EACLlong,
+  author    = {Mart\'{i}nez-G\'{o}mez, Pascual  and  Mineshima, Koji  and  Miyao, Yusuke  and  Bekki, Daisuke},
+  title     = {On-demand Injection of Lexical Knowledge for Recognising Textual Entailment},
+  booktitle = {Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 1, Long Papers},
+  month     = {April},
+  year      = {2017},
+  address   = {Valencia, Spain},
+  publisher = {Association for Computational Linguistics},
+  pages     = {710--720},
+  url       = {http://www.aclweb.org/anthology/E17-1067}
+}
+```
+
 ## The English semantic model declared as semantic templates:
 
 * Koji Mineshima, Pascual Martínez-Gómez, Yusuke Miyao, Daisuke Bekki. Higher-order logical inference with compositional semantics. Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pages 2055–2061, Lisbon, Portugal, 17-21 September 2015. [pdf](http://www.aclweb.org/anthology/D15-1244)

coqlib.v

@@ -0,0 +1,266 @@
+(* Basic types *)
+Parameter Entity : Type.
+Parameter Event : Type.
+
+Parameter Rel : Entity -> Entity -> Prop.
+Parameter Prog : Prop -> Prop.
+Parameter two : Entity -> Prop.
+Parameter _people : Entity -> Prop.
+
+(* Temporal operators *)
+Parameter Hold : Event -> Prop.
+Parameter Cul : Event -> Prop.
+Parameter Past : Event -> Prop.
+Parameter Future : Event -> Prop.
+
+(* Thematic roles *)
+Parameter Subj : Event -> Entity.
+Parameter Top : Event -> Entity.
+Parameter Acc : Event -> Entity.
+Parameter AccI : Event -> Prop -> Prop.
+Parameter AccE : Event -> Event.
+Parameter Dat : Event -> Entity.
+Parameter Attr : Event -> Entity.
+Parameter Deg : Event -> Entity.
+
+(* for underspecified terms *)
+Parameter ArgOf : Entity -> Entity -> Prop.
+
+Parameter _in_front_of : Event -> Entity -> Prop.
+
+(* Generalized quantifiers *)
+Parameter Most : (Entity -> Prop) -> (Entity -> Prop) -> Prop.
+
+Notation "'most' x ; P , Q" := (Most (fun x => P) (fun x => Q))
+   (at level 30, x ident, right associativity) : type_scope.
+
+Axiom most_ex_import :
+  forall (F G: Entity -> Prop),
+   (Most F G -> exists x, F x /\ G x).
+
+Axiom most_consv :
+  forall (F G: Entity -> Prop),
+   (Most F G -> Most F (fun x => (F x /\ G x))).
+
+Axiom most_rightup :
+  forall (F G H: Entity -> Prop),
+   ((Most F G) ->
+   (forall x, G x -> H x) -> (Most F H)).
+
+Hint Resolve most_ex_import most_consv most_rightup.
+
+(* veridical predicates *)
+Parameter _true : Prop -> Prop.
+
+Axiom veridical_true : forall P, (_true P -> P).
+
+Ltac solve_veridical_true :=
+  match goal with
+    H : _true _ |- _
+    => try apply veridical_true in H
+  end.
+
+(* anti-veridical predicates *)
+Parameter _false : Prop -> Prop.
+
+Axiom antiveridical_false : forall P, (_false P -> ~P).
+
+Hint Resolve antiveridical_false.
+
+Ltac solve_antiveridical_false :=
+  match goal with
+    H : _false _ |- _
+    => try apply antiveridical_false in H
+  end.
+
+(* implicative verbs *)
+Parameter _manage : Event -> Prop.
+
+Axiom implicative_manage : forall v : Event, forall P : Prop, AccI v P -> _manage v -> P.
+
+Ltac solve_implicative_manage :=
+  match goal with
+    H1 : _manage ?v, H2 : AccI ?v _ |- _
+    => try apply implicative_manage in H2
+  end.
+
+Parameter _fail : Event -> Prop.
+
+Axiom implicative_fail :  forall v : Event, forall P : Prop, AccI v P -> _fail v -> ~ P.
+
+Ltac solve_implicative_fail :=
+  match goal with
+    H : _fail ?v, H2 : AccI ?v _ |- _
+    => try apply implicative_fail in H2
+  end.
+
+(* factive verbs *)
+Parameter _know : Event -> Prop.
+
+Axiom factive_know : forall v : Event, forall P : Prop, AccI v P -> _know v -> P.
+
+Ltac solve_factive :=
+  match goal with
+    H1 : _know ?v, H2 : AccI ?v _ |- _
+    => try apply factive_know in H2
+  end.
+
+(* privative adjectives *)
+Parameter _former : Prop -> Prop.
+Axiom privative_former : forall P, (_former P -> ~P).
+
+Ltac solve_privative_former :=
+  match goal with
+    H : _former _ |- _
+    => try apply privative_former in H
+  end.
+
+Parameter _fake : Prop -> Prop.
+Axiom privative_fake : forall P, (_fake P -> ~P).
+
+Ltac solve_privative_fake :=
+  match goal with
+    H : _fake _ |- _
+    => try apply privative_fake in H
+  end.
+
+(* before and after *)
+Parameter _before : Event -> Event -> Prop.
+Parameter _after : Event -> Event -> Prop.
+
+Axiom transitivity_before : forall v1 v2 v3 : Event,
+  _before v1 v2 -> _before v2 v3 -> _before v1 v3.
+
+Axiom transitivity_after : forall v1 v2 v3 : Event,
+  _after v1 v2 -> _after v2 v3 -> _after v1 v3.
+
+Axiom before_after : forall v1 v2 : Event,
+  _before v1 v2 -> _after v2 v1.
+
+Axiom after_before : forall v1 v2 : Event,
+  _after v1 v2 -> _before v2 v1.
+
+Hint Resolve transitivity_before transitivity_after before_after after_before.
+
+
+(* Preliminary tactics *)
+
+Ltac apply_ent :=
+  match goal with
+    | [x : Entity, H : forall x : Entity, _ |- _]
+     => apply H; clear H
+  end.
+
+Ltac eqlem_sub :=
+  match goal with
+    | [ H1: ?A ?t, H2: forall x, @?D x -> @?C x |- _ ]
+     => match D with context[ A ]
+         => assert(C t); try (apply H2 with (x:= t)); clear H2
+    end
+  end.
+
+Axiom unique_role : forall v1 v2 : Event, Subj v1 = Subj v2 -> v1 = v2.
+Ltac resolve_unique_role :=
+  match goal with 
+    H : Subj ?v1 = Subj ?v2 |- _
+    => repeat apply unique_role in H
+  end.
+
+Ltac substitution :=
+  match goal with
+    | [H1 : _ = ?t |- _ ]
+      => try repeat resolve_unique_role; try rewrite <- H1 in *; subst
+    | [H1 : ?t = _ |- _ ]
+      => try resolve_unique_role; try rewrite H1 in *; subst
+  end.
+
+Ltac exchange :=
+  match goal with
+    | [H1 : forall x, _, H2 : forall x, _ |- _]
+     => generalize dependent H2
+  end.
+
+Ltac exchange_equality :=
+  match goal with
+    | [H1 : _ = _, H2: _ =  _ |- _]
+     => generalize dependent H2
+  end.
+
+Ltac clear_pred :=
+  match goal with
+    | [H1 : ?F ?t, H2 : ?F ?u |- _ ]
+     => clear H2
+  end.
+
+Ltac solve_false :=
+  match goal with
+    | [H : _ -> False |- False]
+     => apply H
+  end.
+
+(* Main tactics *)
+
+Ltac nltac_init :=
+  try(intuition;
+      try solve_false;
+      firstorder;
+      repeat subst;
+      firstorder).
+
+Ltac nltac_base := 
+  try nltac_init;
+  try (eauto; eexists; firstorder);
+  try repeat substitution;
+  try (subst; eauto; firstorder; try congruence).
+
+Ltac nltac_axiom :=
+ try first
+   [solve_veridical_true |
+    solve_antiveridical_false |
+    solve_implicative_manage |
+    solve_implicative_fail |
+    solve_factive |
+    solve_privative_former |
+    solve_privative_fake
+   ].
+
+Ltac nltac_set :=
+  repeat (nltac_init;
+          try repeat substitution;
+          try exchange_equality;
+          try repeat substitution;  
+          try eqlem_sub).
+
+Ltac nltac_set_exch :=
+  repeat (nltac_init;
+          try repeat substitution;
+          try apply_ent;
+          try exchange;
+          try eqlem_sub).
+
+Ltac nltac_final :=
+  try solve [repeat nltac_base | clear_pred; repeat nltac_base].
+
+Axiom urevent : Event.
+Ltac ap_event := try apply urevent.
+
+Ltac solve_gq :=
+  match goal with
+    H : Most _ _ |- _
+    => let H0 := fresh in
+       try solve [         
+          pose (H0 := H); eapply most_ex_import in H0;
+            try (nltac_set; nltac_final) |
+          pose (H0 := H); eapply most_consv in H0;
+            eapply most_rightup in H0;
+            try (nltac_set; nltac_final) |
+          pose (H0 := H); eapply most_consv in H0;
+            try (nltac_set; nltac_final) |
+          pose (H0 := H); eapply most_rightup in H0;
+            try (nltac_set; nltac_final) ]
+  end.
+
+Ltac nltac :=
+  try solve
+    [nltac_set; nltac_final].
+